Comment by godelski

You have to actually read more than the first line of a Wikipedia article to understand it

  > formal theorem proving

You're using Coq and Lean?

I'm actually not convinced you read the paper. It doesn't have anything to do with your argument. Someone using LLMs with formal verification systems is wildly different than LLMs being formal verification systems.

This really can't work if you don't read your own sources