3 ms·
As 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 mathematic
by olmo23 3mo ago
As 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 3mo agoOr we just don't use LEAN but something better.
- rowanG077 3mo 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 3mo 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 3mo ago[deleted]
- baq 3mo agopay attention to this one https://higherorderco.com/ https://higherorderco.com/ and wait for bend2 announcements