Hacker News
new
|
past
|
comments
|
ask
|
show
|
jobs
|
submit
login
xvilka
on Sept 30, 2019
|
parent
|
context
|
favorite
| on:
Theorem Proving in Lean [pdf]
It's notable, that Coq has more libraries and useful extensions. And they merged Ltac2 into the master, so tactics writing should be better soon.
Join us for
AI Startup School
this June 16-17 in San Francisco!
Guidelines
|
FAQ
|
Lists
|
API
|
Security
|
Legal
|
Apply to YC
|
Contact
Search:
