|
|
|
|
|
|
by jksk61
1003 days ago
|
|
|
well, for lean I know there's a discord (with a fair amount of experts) and a fair share of resources nowadays. However, I did try 3 years ago and the jump between solving a simple algebra proof and contributing to Mathlib (or even understand something in it), is quite high. Coq is well designed/easy to understand but it is missing a core mathlib like Lean. Moreover, most proofs are designed to "compile" quickly and not to be human readable. |
|
|