Show HN: Reducing an OpenAI proof by 25% in a few hours

Category: devtools

Tags: lean, proof-assistant, ai-agents, formal-verification, code-reduction

Score: 4.3/10 (Innovation: 4, Technical: 4, Documentation: 6, Utility: 3)

An experiment that uses AI agents to automatically simplify a large Lean proof by 25% through iterative refactoring, demonstrating that LLM-driven proof minimization is possible. The project is a niche exploration of AI-assisted formal verification, interesting for its specific application but limited in broader impact.

Target audience: formal verification researchers, proof engineers, AI-assisted programming enthusiasts

Repository: https://github.com/offline-ant/wiggums-proof-loop · Lean · Apache-2.0 · 2 stars

View on Hacker News