First Proof

Stream: new members

[Lu-Ming Zhang]

In the first proof document, I don't understand the following content. Could anyone please give me some detailed explanations (like the functions of the commands, the constructions of the commands)?
image.png

[Ruben Van de Velde]

Lean is both a tool for constructing mathematical proofs, and a programming language. Those lines say roughly "we're only going to do mathematics (with classical logic), so ignore some issues that are only relevant for programming"

[Alex Zhang]

What does "noncomputable theory" mean? What is the function of that?

[Julian Berman]

There's some info in these two pages I think that you may find interesting:

https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html
https://leanprover.github.io/theorem_proving_in_lean/type_classes.html#decidable-propositions

[Julian Berman]

(the first on computability, which noncomputable theory affects, and the second on constructive vs. classical logic, which open_locale classical affects)

[Riccardo Brasca]

It means that you can give a definition of foo without giving a true algorithm to compute foo. For example, for any positive integer k¸we know that there is an integer f k such that all natural numbers can be written using at most f k powers (for example all numbers are the sum of 4 squares). This f is, for a mathematician , a perfectly defined function (take f k minimal if you want). But there is no algorithm to compute it, at least not in this definition

[Kevin Buzzard]

Actually it's a tricky theorem that there is an algorithm to compute Riccardo's f, because for k>=3 it turns out that basically the hardest number to write as a sum of k'th powers is the number just less than the largest multiple of 2^k which is less than 3^k (e.g. 23 is hard to write as a sum of natural cubes, you'll need 9, and f(3)=9). This of course doesn't change the fact that one wants to be able to reason about the function without proving the hard theorem I just mentioned above. No algorithm is known to compute the "all sufficiently large n" version of Riccardo's function (which is actually Waring's function -- all sufficiently large naturals are definitely the sum of 7 natural cubes, it is conjectured that all n>7373170279850 are the sum of 4 natural cubes, but whether the "magic number" for cubes is 4, 5, 6 or 7 is unknown. Andrej Bauer pointed out to me that you can make this function computable, but it then maps to a target space which is not computably isomorphic to the naturals (but which is classically isomorphic to them).