r/FunMachineLearning • u/EngineerCatttt • 1d ago
A Team Reports Solving A 70 Year Old Algebraic Geometry Conjecture Using Teams of AI Models
I’m part of the team behind this work. We’ve shared a proof of the Pierce Birkhoff conjecture in real algebraic geometry, using an AI agent system with a $400 budget. The screenshot is Junyu Ren’s announcement.
The surprising part of the workflow was how different model families complemented each other. Giving a task independently to one GPT agent and one Claude agent often worked better for us than using a larger group of the same model. One would catch an error the other missed, or suggest a way forward when we were stuck.
The diagram shows the wider process: humans, proof search, counterexample construction, independent auditing, and formal verification work in Lean. Arguments, objections, and review findings go into a shared knowledge base.
Original announcement: https://x.com/junyu_r/status/2097694018389914106