3 ms·

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.

by svara 8mo ago

nwyin 8mo ago
it's a bit dated, but Terence Tao has a video of formalizing a proof with LLMs from 9 months ago which should be illuminating https://youtu.be/zZr54G7ec7A?si=-l3jIZZzfghoqJtq https://youtu.be/zZr54G7ec7A?si=-l3jIZZzfghoqJtq
- Gehinnn 8mo ago
  This is very similar to how I worked with Lean a year ago (of course in a much simpler domain) - mostly manual editing, sometimes accepting an inline completion or next edit suggestion. However, with agentic AI that can run lean via CLI my workflow changed completely and I rarely write full proofs anymore (only intermediate lemma statements or very high level calc statements).
  - pvillano 8mo ago
    Do lean poofs need to be manually reviewed? 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?
    - Gehinnn 8mo ago
      There have been bugs in Lean that allowed people to prove False, from which you can prove anything (they have been fixed). 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.
Gehinnn 8mo ago
Here is a session that I just had with AI: https://gist.github.com/hediet/e3569a7c6b4b7c4f7d4a7db4101047de https://gist.github.com/hediet/e3569a7c6b4b7c4f7d4a7db410104... (summarized by AI). And here are some examples of the different philosophies of AI proofs and human proofs: https://gist.github.com/hediet/e3569a7c6b4b7c4f7d4a7db4101047de#file-2_human_vs_ai-lean 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)

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.

by svara 8mo ago

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.

nwyin 8mo ago

it's a bit dated, but Terence Tao has a video of formalizing a proof with LLMs from 9 months ago which should be illuminating https://youtu.be/zZr54G7ec7A?si=-l3jIZZzfghoqJtq https://youtu.be/zZr54G7ec7A?si=-l3jIZZzfghoqJtq

Gehinnn 8mo ago
This is very similar to how I worked with Lean a year ago (of course in a much simpler domain) - mostly manual editing, sometimes accepting an inline completion or next edit suggestion. However, with agentic AI that can run lean via CLI my workflow changed completely and I rarely write full proofs anymore (only intermediate lemma statements or very high level calc statements).
- pvillano 8mo ago
  Do lean poofs need to be manually reviewed? 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?
  - Gehinnn 8mo ago
    There have been bugs in Lean that allowed people to prove False, from which you can prove anything (they have been fixed). 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.

Gehinnn 8mo ago

Here is a session that I just had with AI: https://gist.github.com/hediet/e3569a7c6b4b7c4f7d4a7db4101047de https://gist.github.com/hediet/e3569a7c6b4b7c4f7d4a7db410104... (summarized by AI). And here are some examples of the different philosophies of AI proofs and human proofs: https://gist.github.com/hediet/e3569a7c6b4b7c4f7d4a7db4101047de#file-2_human_vs_ai-lean 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)