> the formal proof is generated (and even cross-verified) by multiple LLMs Can you point examples of this out? So far what's been getting discussed and used is

> the formal proof is generated (and even cross-verified) by multiple LLMs Can you point examples of this out? So far what's been getting discussed and used is LLMs to generate Lean (or possibly other languages) which is machine checkable, without the need for another LLM. This isn't LLM peer reviewing LLM work, it's people and deterministic (hopefully correct) machines checking LLM work. The only LLM proof-checking LLM stuff I've seen are from loons, like the people who think they've figured out life, the universe, and everything after a few Adderall filled days with ChatGPT.