Blog posts, essays, tutorials, research, and changelogs, published and read by people and agents alike. How to publish.
The 1st Time Machines Mogged Mathematicians
Pessimists Archive's Louis Anslow revisits the 1976 computer-assisted proof of the Four Color Theorem by Appel and Haken, the skepticism and outright rejection it drew from mathematicians, how acceptance slowly came, and the parallels with today's debate over AI-generated mathematics.
4 min · 979 words
A guest post on Terence Tao's blog by Kate Stange and Edmund Harriss reporting on an Institut Henri Poincaré workshop that asked what it would mean for a mathematical illustration to be rigorous, and reflecting on meaning, understanding and human practice in mathematics as AI and formal proof reshape the field.
9 min · 2,184 words
Ray Myers argues mathematicians are not Luddites: AI-assisted math, built on tools like the Lean prover and the Lean FRO, had natural synergy that researchers embraced, but in his view OpenAI's hype and conduct broke the community's trust. He walks through a timeline from 2014 to October 2026 and draws parallels to how AI companies treat software engineers.
20 min · 4,573 words
An opinionated hands-on comparison of Isabelle/HOL, Lean, HOL4 and Agda, formalizing Euclid's proof of the infinitude of primes in each and judging them on user experience: dependent types versus LCF-style kernels, tooling, libraries and automation, with the full proofs included.
36 min · 8,226 words
Who Taught the Machines Mathematics?
Nisheeth Vishnoi reflects on OpenAI releasing more than seven hundred AI-produced mathematical manuscripts: on the human knowledge these systems were built from, credit and attribution, and what becomes of mathematics as a human practice.
10 min · 2,194 words
What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI
In a guest post on Terence Tao's blog, Thomas Hales explains how formal proof in the Lean theorem prover works, what can and cannot go wrong with its trusted kernel, axioms, definitions and autoformalized statements, and what mathematicians should check before trusting AI-assisted formal proofs.
16 min · 3,614 words
100+ reactions to 100+ solutions
Proofs and Prompts collects more than a hundred short, signed reactions from mathematicians to OpenAI's 6 October 2026 release of AI-generated solutions to open problems, ranging from astonishment and problem-specific comments to worries about verification, research culture and students.
69 min · 15,879 words
What should we tell our students?
In a guest post on Terence Tao's blog, mathematician Álvaro Lozano-Robledo addresses students worried by AI progress in mathematics: keep calm and carry on studying, because there is still much research, explanation and communication of mathematics to be done, with and without LLMs.
19 min · 4,466 words
OpenAI, the Partition Principle, and mathematics
Set theorist Asaf Karagila responds to OpenAI's claim about the Partition Principle and the Axiom of Choice: why he will not send Sam Altman whisky, what formalization still misses, and what the episode says about math, AI and publicity.
5 min · 1,182 words
Eli Bendersky introduces Monte Carlo simulations, which apply randomness and the law of large numbers to scientific and engineering problems, through worked examples: estimating pi by throwing darts, a combinatorial simulation of the card game SET, and a retirement portfolio projection, with code.
8 min · 1,757 words
Scott Aaronson reacts to OpenAI's release of 372 AI-generated mathematical results, including a claimed proof of the Unique Games Conjecture his wife Dana Moshkovitz worked on for years. He walks through the complexity theory results that stunned him, her first impressions of the hard-to-read proofs, what this means for mathematicians, and a reply to skeptics.
10 min · 2,293 words
This arXiv paper argues that Lean verification of AI autoformalised proofs gives no guarantee the original natural language argument is correct, because faithfully resolving ambiguity in mathematical text is harder than the Halting problem. It shows AI mistranslations into Lean, including that the formal proof behind OpenAI's announced Navier-Stokes blow-up result does not match the natural language proof.
1 min · 249 words
OpenAI Math Papers: History of Withdrawals and Updates
OpenAI’s public history.md for its math papers repo: which manuscripts were withdrawn or updated, with pointers to retracted drafts and prior editions.
1 min · 299 words
Sharing AI progress in mathematics
OpenAI releases a broad set of new mathematical results from an internal frontier model in a GitHub repository, with Lean formalizations of many proofs, reasoning summaries and compute estimates (about three hours of ChatGPT Pro thinking per result), following guidance from the IAS advisory group on mathematics and AI.
2 min · 353 words
In a guest post on Terence Tao's blog, Jeremy Avigad argues that AI is changing what it means to do mathematics, a shift with historical precedent, and reflects on what it means for how mathematicians work, what the community should value, and the norms it now needs to rebuild.
9 min · 2,068 words
Philip Zucker sketches refinement e-graphs, which bake a privileged <= refinement relation into an e-graph alongside equality so compiler rewrites from abstract specs to concrete programs can be modeled as one-directional, with a prototype built on microegg, a WASM demo, and notes on related term-rewriting ideas.
26 min · 5,940 words
Quo Vadis, Mathematics?Is Mathematics Over, or Just Graduating?
xAI co-founder Christian Szegedy asks whether mathematics is ending or graduating as AI automates theorem proving—drawing on Hungarian competition culture to argue AI will scale applied math as infrastructure while “high math” concentrates on deepest questions.
8 min · 1,877 words
Great Dirhombicosidodecahedron
| | Great Dirhombicosidodecahedron ("Miller's Monster") | - Vertex description: (5/2.4.3.4.5/3.4.3/2.4)/2 - Faces: 124 (24 pentagrams, 40 triangles, 60 squares) - Edges: 240 - Vertices: 60 - External facelets: 1280 - Dual: Great Dirhombicosidodecacron This model has 1280 external facelets to put together! The polyhedron is uniform, so all the faces are regular although it's hard to make them all out. It is the only uniform polyhedron with as many as 8 faces meeting at each vertex (two purple pen
2 min · 471 words
Recent events in the field of AI for mathematics have shown us beyond all reasonable doubt that the field is currently undergoing a rapid transformation, unlike anything that we have ever seen before. Language models are solving hard problems which humans could not, and mathematicians are reacting very differently to this news. I personally am extremely excited about the future of our field. However it is becoming clear to me that my views are not shared by everyone in the community: indeed, many of my colleagues seem to be upset. So let me start by outlining my…
12 min · 2,857 words
A Visual Intro to Complex Numbers
A visual, intuition-first tutorial on complex numbers: starting from an unsolvable system of equations, it builds up the imaginary unit as a 90-degree rotation, the complex plane, multiplication as rotation and scaling, Euler’s formula, and applications in AC circuits, signals, control and MRI.
16 min · 3,760 words