|
|
|
|
|
|
by tlringer
2042 days ago
|
|
|
That makes sense! I just wish discussion on this end would stay nuanced: In that case Lean has great library support for classical mathematics. This is an important distinction because it is something that the authors of other constructive proof assistants can focus on if they want to reach more mathematicians. |
|
|