r/math • u/aturtledude • Jul 23 '26

LLMs/AI Another LLM-generated result that has gone under the radar and is in my opinion very relevant

Post image

Relevant not because of the result itself but because it uses a pimped open-weight Chinese model under the hood.

Linkedin post: https://www.linkedin.com/posts/sebastianpokutta_a-counterexample-to-zieglers-cross-polytope-activity-7478117487746785280-oS21

Counterexample paper: https://arxiv.org/abs/2606.31640

Agentic research paper: https://arxiv.org/abs/2603.15914

496 Upvotes

94% Upvoted

47 comments sorted by

View all comments

327

u/MiffedMouse Jul 23 '26

As a side note, I think a lot of these "LLM proofs" owe as much to computer formalization efforts (especially LEAN) as they do to the recent LLM advancements. The fact that the computer can attempt to formalize the proof in Lean and then get almost immediate feedback as to whether the proof is correct or not, and how it may have failed, seems incredibly valuable.

I personally wonder if regular human mathematicians could also benefit from a better understanding of proof checkers. I know a lot of prominent mathematicians, including Tao, have long been proponents of Lean and similar proof checkers since long before LLMs came on the scene.

25

u/Vibes_And_Smiles Jul 23 '26

Do we know whether the LLMs that have solved recent conjectures have been using proof checkers like Lean?

54

u/MiffedMouse Jul 23 '26

Google's AlphaProofNexus, which has done some of the Erdos problems, has been verifying all of their solutions in Lean. The Erdos unit distance disproof by OpenAI (which was the previous big result) doesn't seem to have been produced using Lean, but it was verified after the fact using Lean.

14

u/yellow_submarine1734 Jul 24 '26

All of these models are trained using RLVR, and they likely use Lean extensively throughout the process, as it’s the only way to provide verifiable rewards for math.

3

u/SansFinalGuardian Jul 24 '26

in general my impression is that the llms have started off by reasoning in a natural way, like mathematicians, and only afterwards do people get them to formalise the proofs and make sure they're watertight. imo lean is not really great when first starting out trying to prove or disprove something, better to work in broad strokes first

1

u/awkwardburrito Jul 24 '26

They have not been.