3 ms·
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 p
by enricozb 1y 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.