lean

> For example, we have mathematics without the law of the excluded middle and with it, ones without the axiom of choice and with it, etc. This is a bit off-topic. Elsewhere in comments [1] people talk about Terence Tao and his recent work in Lean. Lean is based on intuitionistic logic, a base which doesn't include axiom of choice and the excluded middle. Since Tao and other classical mathematicians need excluded middle for proofs by contradiction. The Classical library in Lean starts by declaring axiom of choice [2] and after some lemmas introduces excluded middle as a theorem, called "em" for brevity [3]. I like how Lean makes this particular choice for classical mathematics very obvious. [1] https://news.ycombinator.com/item?id=38102096#38104412 [2] https://github.com/leanprover-community/lean/blob/cce7990ea8... [3] https://github.com/l

I'm confused by "postulating an axiom doesn't count". Are you aware that choice is an axiom in Lean? https://github.com/leanprover-community/lean/blob/master/lib...

For people interested in using Lean, note that there's a community fork (https://github.com/leanprover-community/lean) of the last official Lean 3 release 3.4.2 (https://github.com/leanprover/lean). The fork is still under active maintenance, so might be a better place to start (the main development team have moved onto developing Lean 4.0 (https://github.com/leanprover/lean4), and it's not clear when that will be ready).