alt Hacker NewsThis 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).
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?