ParentFull threadKK7NIL·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/e049IoFBnLAView on HN