7 ms·
I’m doing this by working all logical steps into lean (formal verification) the quick feedback loop between the AI prose and the Lean verification errors and wa
by ibarrajo 2mo ago
I’m doing this by working all logical steps into lean (formal verification) the quick feedback loop between the AI prose and the Lean verification errors and warnings ensures that its logically consistent.
The issue that remains are two things, ensuring the idea of the proof is actually the thing you want to prove and the interpretation of the results you get. But besides that, everything inside of the kernel checked code is logically consistent
- iib 2mo agoIn my experience, lean will show that it's correct, but does it not lose the mathematical intuition that led to the result? As far as my experience goes, that's really hard to encode in lean itself. Could we maybe get more information about the problem from the LLM trace itself here?
- olmo23 2mo agoAs proofs become more and more complex, we will need two AI pipelines: one to generate the LEAN proof, and a second one to extract useful lessons for mathematicians from the LEAN proof.
- auggierose 2mo agoOr we just don't use LEAN but something better.
- rowanG077 2mo agoDoes anything truly better exist? I'm not a mathematician but I did use Rocq and Lean during university. And I found lean to be better.
- auggierose 2mo agoNo, something truly better does not exist yet, but that doesn't mean that it won't. Lean is young compared to Isabelle or Rocq, but actually quite old in absolut terms (and especially in AI terms).
- deleted 2mo ago[deleted]
- baq 2mo agopay attention to this one https://higherorderco.com/ https://higherorderco.com/ and wait for bend2 announcements