Hacker News
new
|
past
|
comments
|
ask
|
show
|
jobs
|
submit
login
auggierose
59 days ago
|
parent
|
context
|
favorite
| on:
Claude Fable produced a counterexample to the Jaco...
Or we just don't use LEAN but something better.
rowanG077
59 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.
auggierose
59 days ago
|
parent
|
next
[–]
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
59 days ago
|
parent
|
prev
[–]
pay attention to this one
https://higherorderco.com/
and wait for bend2 announcements
Guidelines
|
FAQ
|
Lists
|
API
|
Security
|
Legal
|
Apply to YC
|
Contact
Search:
