Here is a session that I just had with AI: https://gist.github.com/hediet/e3569a7c6b4b7c4f7d4a7db4101047de https://gist.github.com/hediet/e3569a7c6b4b7c4f7d4a7d

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)