Tag
In a Numberphile interview, Fields Medalist Terence Tao discusses mathematics entering an industrialized era, moving from “proof scarcity” to “proof abundance,” the misalignment of incentives between AI companies and academia, and the risk of human understanding being sidelined.
A commentary questioning whether AI proof generation alone can replace mathematicians, contrasting Anthropic's Fermat project and OpenAI's math release with the harder challenge of reliably explaining and connecting new results.
OpenAI released a repository containing 722 mathematical manuscripts (700 preprints) grouped into 372 families of proofs and counterexamples generated by an unreleased internal model, along with some Lean formalizations and abridged reasoning traces. The results span areas like the Riemann zeta function, Mahler conjectures, and free group factors, and were produced using roughly three hours of ChatGPT Pro thinking compute per result on about 4,000 posed problems.
A tutorial-style walkthrough for software engineers that formalizes a constructive proof about regular languages in the Lean theorem prover, explaining specification, implementation, induction, and the anatomy of a formal proof step by step. The piece demonstrates how Mathlib's existing theorems make formalizing textbook automata theory accessible to developers.
OpenAI used an internal model, Astra, to solve ten mathematical problems that had stalled for over a decade, spending under $2,000 per problem and releasing Lean 4 formalizations and a paper. The results prompt reflections on AI's role in mathematics.
PriorProof introduces a method to measure the novelty of proof techniques in formal mathematics by analyzing the dependency footprint of Lean proof terms against a prior built from an earlier snapshot of Mathlib. The method agrees with human raters on 69.7% of pairs and provides interpretable score gaps.
The Ramanujan Challenge for AI, launched by the Ramanujan Machine, presents ten research-level problems on explicit formulas for mathematical constants, testing whether AI systems can produce valid formal proofs or symbolic derivations. The challenge runs until August 1, 2026, and accepts submissions in formal proofs, CAS-based derivations, or human-readable proofs with reproducible code.