Can you give some examples of this? Maybe have something online? I would love to learn more about how to do proof driven AI assisted development.
And here are some examples of the different philosophies of AI proofs and human proofs: https://gist.github.com/hediet/e3569a7c6b4b7c4f7d4a7db410104...
I use VS Code in a beefy Codespace, with GitHub Copilot (Opus 4.5). I have a single instruction file telling the AI to always run "lake build ./lean-file.lean" to get feedback.
(disclaimer: I work on VS Code)
Or is it as long as you formalize your theorem correctly, a valid lean program is an academically useful proof?
Are there any minimal examples of programs which claim to prove the thing without actually proving the thing in a meaningful way?
Otherwise, if you check that no custom axiom has been used (via print axioms), the proof is valid.
It's easy to construct such an example: Prove that for all a, b, c and n between 3 and 10^5, a^n=b^n+c^n has no solution. The unmeaningful proof would enumerate all ~10^20 cases and proof them individually. The meaningful (and probably even shorter) proof would derive this from Fermat's theorem after proving that one.