[KK7NIL]

They use LLMs to help write formal proofs (in languages like Coq) that are then checked by traditional programs; they're not using AI as the checker.

https://youtu.be/e049IoFBnLA