[nwyin]

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

[Gehinnn]

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]

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?