Howardism · Vol. 03Plate II · No. 02
AI For Mathematics, tagged.
Notes5TagAI For MathematicsOldest23 May 2026Newest23 May 2026
Every article tagged ai for mathematics, newest first.
| Title | Summary | Date |
|---|---|---|
| Agentic Loops Overtake Bespoke Systems | DeepMind's *basic* Ralph-loop agent matched its bespoke evolutionary+AlphaProof system as the LLM improved; the bitter lesson / harness-shrinkage confirmed in formal math | |
| AI-Driven Formal Proof Search | LLM generates Lean, compiler verifies every step → eliminates hallucination; DeepMind resolves 9/353 Erdős + 44/492 OEIS open problems; verification as a filter for human review | |
| AlphaProof Nexus | DeepMind framework for LLM-aided Lean proof generation; four agents (basic→full-featured); proof-sketch + EVOLVE-BLOCK interface; SafeVerify | |
| Evolutionary Proof Search | The full-featured agent's mechanism: population DB of proof sketches, Elo via Plackett–Luce/Gibbs, P-UCB selection, LLM-critic fitness for binary proof eval | |
| Lean | Proof assistant whose compiler mechanically verifies every step; the `sorry` placeholder enables proof sketches; mathlib maturity gates the reachable frontier |