For anyone wanting to harness AI models to create formally verified proofs for theoretical alignment, it looks like last call for formalizing question statements.
Game theory is almost completely absent from mathlib4. I found some scattered attempts at formalization in Lean online but nothing comprehensive. This feels like a massive oversight to me—if o12345 were released tomorrow with perfect reasoning ability then I’d have no framework with which to check its proofs of any of my current research questions.
For anyone wanting to harness AI models to create formally verified proofs for theoretical alignment, it looks like last call for formalizing question statements.
Game theory is almost completely absent from mathlib4. I found some scattered attempts at formalization in Lean online but nothing comprehensive. This feels like a massive oversight to me—if o12345 were released tomorrow with perfect reasoning ability then I’d have no framework with which to check its proofs of any of my current research questions.