Post #3054905

RE: https://mastodon.social/@winbuzzer/116640379007256611 This is interesting, and basically the idea I had when I went through a phase of interest in formal proof checkers (in those days it was Coq, not Lean, and some interesring outsiders like Naproche) But of course at that time there was no such thing as LLMs which could guide the formal proof. I can imagine though that there will be a somewhat low ceiling to this kind of approach.