|
|
|
|
|
|
by enricozb
315 days ago
|
|
|
As far as I understand, The lead of this project Kevin Buzzard is a mathematician first. And the majority of mathematicians are untroubled by non-constructive proofs. I would imagine that proof directions that result in the most interesting additions to Mathlib would be chosen. |
|
|