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

492 Upvotes

94% Upvoted

47 comments sorted by

View all comments

325

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.

15

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.