А без аксиомы выбора никак?
На этот вопрос отвечает Кевин Баззард:
Re which parts depend on choice: currently basically all of it, because in Lean choice is assumed by even the most basic tactics, even when it is not necessary. Indeed I just checked and if you prove that 2+2=4 (as real numbers) using mathlib’s `norm_num` tactic then the resulting proof uses the axiom of choice (probably via the law of the excluded middle, which is deduced as a consequence of AC in Lean’s core library). Lean’s mathematics library makes no attempt to do choice-free mathematics. However now the proof exists, it will be possible to start inspecting it and removing unnecessary uses of AC, and asking what fragment of mathematics the proof will live in. A more mathematically interesting observation than the 2+2=4 observation is that the formal proof uses the Langlands–Tunnell theorem, which uses hard analysis, where countable dependent choice is often an essential tool.
