Zulip Chat Archive

Stream: new members

Topic: First Proof


Lu-Ming Zhang (May 23 2021 at 09:02):

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 (May 23 2021 at 10:06):

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 (May 23 2021 at 13:17):

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

Julian Berman (May 23 2021 at 13:33):

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 (May 23 2021 at 13:33):

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

Riccardo Brasca (May 23 2021 at 13:34):

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 (May 23 2021 at 15:00):

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).


Last updated: Dec 20 2023 at 11:08 UTC