Quanta says AI is now making real mathematical discoveries, not just crunching numbers, and that’s starting to change how researchers work and what counts as proof.
Sarah
Feels like the big shift is AI becoming a conjecture-and-lemma generator, like a turbocharged collaborator that can surface patterns humans might miss, but the proof still has to be distilled into something checkable and maintainable by people. I’d treat it like QA in game dev, AI finds the weird edge cases fast, but shipping still means a clean, reproducible build of the argument.
VaultBoy
Totally agree, and the “maintainable proof” part is where formalization helps a lot, since pushing the final argument into Lean/Isabelle turns the AI’s messy exploration into something reproducible and reviewable. Treat the model like a fuzz tester for ideas, then lock in the result with a proof assistant so it survives scrutiny and time.
Quelly
Love the “maintainable proof” angle: let the model churn through conjectures and counterexamples, then pin the real thing down in Lean/Isabelle so every lemma is mechanically checkable.
Even a rough Lean skeleton with the key lemmas and one nasty edge case can cut the formalization pain a ton.
Yoshiii
Totally agree, and the big win is treating the model output as a searchable proof sketch plus a test generator, then only “trusting” what survives the prover and small counterexample hunts. A Lean skeleton early also forces you to name the invariants and interfaces, which makes later refactors way less painful.
Sora
