FLT is a negative statement ("there are no nonzero integers x, y, z such that..."), and proofs by contradiction are constructively valid for proving negative statements.
For what it's worth, I don't think that Kevin Buzzard is the person you should talk to if you are interested in proof assistant design. As far as I know, Buzzard does not consider himself to be an expert in type theory…
AFAICT, this issue only comes up if you form the quotient of a proposition by a relation. But there is no point in doing that (all the proofs of a proposition are already equal!) so it's not an issue in practice and it…
Computation is the difference. In Lean, applying the universal property of the quotient (`Quotient.lift f Hf`) to an element that is of the form `Quotient.mk a` reduces to `f a`. This rule is fine in itself, but the…
There is a nice illustration of a 2-sphere wrapped twice around another 2-sphere on the Wikipedia article for the homotopy groups of spheres [0]. Now, there are many ways of proving that there is only one way (up to…
Good catch, thank you.
That's pretty cool, but the downsides of switching to RRA are not only about user experience. When the result is 0.0000000..., the calculator cannot decide whether it's fine to compute the inverse of that number. For…
If you look at the Wikipedia page for second order arithmetic, there is a definition in the language of first order logic as a two-sorted theory comprising a handful of basic axioms, the comprehension scheme, and the…
The axioms of second order Peano arithmetic are certainly recursively enumerable, in fact you can pick a formulation that only uses a finite number of axioms. And second order arithmetic is much weaker than the type…
FLT is a negative statement ("there are no nonzero integers x, y, z such that..."), and proofs by contradiction are constructively valid for proving negative statements.
For what it's worth, I don't think that Kevin Buzzard is the person you should talk to if you are interested in proof assistant design. As far as I know, Buzzard does not consider himself to be an expert in type theory…
AFAICT, this issue only comes up if you form the quotient of a proposition by a relation. But there is no point in doing that (all the proofs of a proposition are already equal!) so it's not an issue in practice and it…
Computation is the difference. In Lean, applying the universal property of the quotient (`Quotient.lift f Hf`) to an element that is of the form `Quotient.mk a` reduces to `f a`. This rule is fine in itself, but the…
There is a nice illustration of a 2-sphere wrapped twice around another 2-sphere on the Wikipedia article for the homotopy groups of spheres [0]. Now, there are many ways of proving that there is only one way (up to…
Good catch, thank you.
That's pretty cool, but the downsides of switching to RRA are not only about user experience. When the result is 0.0000000..., the calculator cannot decide whether it's fine to compute the inverse of that number. For…
If you look at the Wikipedia page for second order arithmetic, there is a definition in the language of first order logic as a two-sorted theory comprising a handful of basic axioms, the comprehension scheme, and the…
The axioms of second order Peano arithmetic are certainly recursively enumerable, in fact you can pick a formulation that only uses a finite number of axioms. And second order arithmetic is much weaker than the type…