Unfamiliar Terrain
summary
Uses AlphaEvolve to evolve code that generates proof objects, produces a sub-ten-node asymmetric gadget that improves a TSP hardness ratio to 111/110, a 19-node weighted max-4-cut gadget, and new Ramsey lower bounds by constructing large Ramanujan graphs. Fast verifiers (produced and summarized with Gemini) let thousands of candidate checks run in seconds, with exhaustive verification run at the end; some results need hours or days to fully certify.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:44AI in theorem proving
- 5:19AlphaEvolve tool mechanism
- 6:01NP-hardness and graph results
- 8:53Mechanical gadget generation
- 14:56Ramsey numbers lower bounds
- 19:36AI's role and limits
- 24:52Language model invariants
- 27:26Conclusion
related talks
44mAutomated Scientific Discovery Using Insights from Problem Structure
17mNeuro-Symbolic Proof Generation for Scaling Systems Software Verification
26mWeaver: Shrinking the Generation-Verification Gap with Weak Verifiers
01h 16mCoding Agents: New opportunities for formal methods?
43mPushing the Limits of Zero Knowledge Applications
28mHow Does A STARK Proof System Work
22mTowards Automated Verification of LLM-Synthesized C Programs
01h 08mLean: Machine-Checked Mathematics and Verified Programming, Past and Future