Comment by 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