alt Hacker NewsCan 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.
Replies
nwyin • today at 2:27 PM
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
➕ show 1 reply
Here is a session that I just had with AI: 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/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)