Blog — Latest in Math Tech & AI
News, studies, deep-dives, and trends at the intersection of mathematics and AI.
FaithSieve shows why checking AI math proofs needs more than a confident final answer
An August 26, 2026 arXiv paper introduces a Lean-assisted framework for locating the first real error in natural-language mathematical proofs.
A new AI4Math study measures how fast AI is entering mathematical research
An August 25, 2026 arXiv study tracks disclosed AI use across nearly 33,000 mathematics papers and finds rapid but uneven adoption.
Jeremy Avigad asks what mathematics should become as AI turns into a research participant
Posted to arXiv on August 24, 2026, a new essay by Jeremy Avigad argues that recent theorem-proving milestones should widen, not narrow, the conversation about how AI can serve mathematical practice.
An AI-discovered fast dynamo shows mathematical AI edging from benchmark work toward publishable analysis
Posted to arXiv on August 20, 2026, a new analysis-and-probability paper reports a smooth random fast dynamo on the three-torus and states that the central proof idea was generated autonomously by an AI system before human verification and writing.
Terence Tao asks what mathematics should protect as AI reaches research level
Posted to arXiv on August 17, 2026, Terence Tao’s new essay shifts the conversation from whether AI can do mathematics to what mathematicians should still value, teach, and reward when it can.
FAR shifts AI mathematics from solving one chosen problem to searching a whole research direction
Posted to arXiv on August 17, 2026, the FAR pipeline shows how AI can scan mathematical literature, surface open conjectures, attempt them at scale, and send only the strongest artifacts to expert review.
FaithformBench asks whether mathematical autoformalization tools stay faithful when reasoning goes wrong
Posted to arXiv on August 11, 2026, FaithformBench studies whether AI systems that translate mathematical reasoning into Lean preserve both valid and invalid steps instead of silently “fixing” the input.
FormaTheoria turns AI-assisted Lean formalization toward one of mathematics’ biggest long-range targets
Posted to arXiv on August 11, 2026, FormaTheoria presents an AI-assisted workflow for rebuilding large mathematical theories in Lean, using finite-group results tied to the Classification of Finite Simple Groups as a demanding test case.
MechGeo pushes AI geometry further by turning Olympiad diagrams into Lean-checked proofs
Posted to arXiv on August 3, 2026, MechGeo combines autoformalization, counterexample-guided repair, and kernel-checked proving to tackle Euclidean geometry problems in Lean 4.
Showing page 6 of 10 · 86 total