3 ms·
Real mathematicians doesn’t care about constructivist. Also, Lean supports working with both. So you can choose what you want to use.
by mbrodersen 5y ago
Real mathematicians doesn’t care about constructivist. Also, Lean supports working with both. So you can choose what you want to use.
- zozbot234 5y agoThe mathematicians who study topos theory, the 'internal logic' of whatever category etc. are definitely "real" mathematicians, and they have to care about constructive settings because these come up very naturally in that field. Constructivism is not an isolated niche anymore, it interacts with "real" math too.