Y
Hacker News
new
|
ask
|
show
|
jobs
by
auggierose
9 days ago
Or we just don't use LEAN but something better.
1 comments
rowanG077
9 days 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.
link
auggierose
9 days 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).
link
baq
8 days ago
pay attention to this one
https://higherorderco.com/
and wait for bend2 announcements
link