Comment by auggierose 2 months ago Or we just don't use LEAN but something better. 4 comments auggierose Reply rowanG077 2 months ago Does 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 2 months ago No, 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). baq 2 months ago pay attention to this one https://higherorderco.com/ and wait for bend2 announcements
rowanG077 2 months ago Does 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 2 months ago No, 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). baq 2 months ago pay attention to this one https://higherorderco.com/ and wait for bend2 announcements
auggierose 2 months ago No, 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).
baq 2 months ago pay attention to this one https://higherorderco.com/ and wait for bend2 announcements
Does 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.
No, 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).
pay attention to this one https://higherorderco.com/ and wait for bend2 announcements