Blog — Latest in Math Tech & AI
News, studies, deep-dives, and trends at the intersection of mathematics and AI.
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.
BlueprintRepair turns failed Lean proof plans into smaller, cheaper AI repair jobs
Submitted to arXiv on July 30, 2026, a new formal-mathematics study shows that schema-checked local edits can repair failed Lean proof blueprints almost as effectively as free-form rewrites while using fewer tokens.
From lecture notes to Lean, a probability textbook becomes a checkable AI-era math resource
Submitted to arXiv on July 29, 2026, a new Lean formalization project argues that turning a probability textbook into machine-checked mathematics can strengthen both teaching and reliable AI-assisted proof work.
Nature warns that AI in mathematics needs rules before bad habits harden
Published on July 27, 2026, a new Nature World View argues that mathematics should set stronger norms for AI use now, before opaque tools, weak attribution, and low-quality machine-written papers become routine.
A learned Lean 4 tactic shows a cautious new path for AI inside formal proofs
Posted to arXiv on July 25, 2026, a new formal-mathematics paper shows how learned interventions can help Lean 4’s `grind` tactic solve harder theorems without disrupting proofs it already handled reliably.
AI-assisted Lean formalization turns a kinetic-theory proof into a checkable artifact
Dated July 22, 2026 on arXiv, a new case study shows how a mathematician-guided AI workflow formalized the Vlasov equation in Lean 4 and made the proof machine-checkable.
Showing page 4 of 7 · 63 total