Fun fact, there have been 3 soundness bugs in lean 4 so far. (They were all fixed within hours.) I expect we have not yet found them all, but I also do not sleep poorly worried that mathematics will come tumbling down,…
Should I introduce you to https://arxiv.org/abs/2403.14064 ?
If this is your situation, you should absolutely be asking more questions on Zulip. It is really easy to get guidance on how to use mathlib, what things exist and where they are. The issue with stacked casts is mostly…
No, Lean is not suitable for axiomatic investigations, it comes with too much baggage from "classical foundations". As Randall said above, Lean is axiomatically much stronger than NF, and that's even with "no axioms"!…
> Speaking of Miri, is the long term goal to say for certain whether or not a program execution encountered UB? (Which is, of course, different than verifying it before execution at compile time.) That's more than a…
Yes, that is incorrect. If you write `partial def foo : Nat := foo + 1` it will be accepted, but `def foo : Nat := foo + 1` is not. So while lean checks that functions terminate by default, it is possible to define and…
The jargon is a bit confusing sometimes. In Lean, "refl" does a whole lot more than prove x=x. It is of course available if you want to prove x=x, but the real power of "refl" is that it also proves x=y where x and y…
> implementation in C++ rather than a nice functional language for dogfooding To be fair, the main author of Lean has been cloistered for two years writing the next version, Lean 4, which is written in its own (pure…
For those who are more into watching talks on YouTube than reading papers, and are interested in the low level hardware formalization aspect of this project, there is a recording of the ITP 2019 presentation here: "x86…
It does, but only if you state the theorem in a particular way. Let's say that you have a verifier A, that checks theorems in Peano Arithmetic (PA). Inside that logic, you can define what a computer is, how it executes,…
(I'm the author of the paper BTW.) Regarding TLA+ and CakeML: TLA+ seems like a good idea, Leslie Lamport talks a lot of sense in most of his papers. I especially recommend "Composition: A Way to Make Proofs Harder"…
Metamath has tactics, but they aren't part of metamath per se; they are part of the tools that you use to write proofs. You don't make the rest of the world run the same proof search you did hundreds of times, finding…
Software gets more complicated, and so bugs become more common. Hardware gets faster, so speed pressures are reduced on software, so it gets more layered and hence slower; and also more complicated. More layers of…
What if your brain is the bottleneck?
It goes without saying that metamath is not designed to be read from the source directly. To be perfectly fair, Coq isn't either; you can kind of get the gist but to really understand what's going on you have to start…
The verification of entire proof libraries (like the entire Coq standard library, or the Isabelle Archive of Formal proofs) usually ranges from hours to days, as do some of the larger computer science projects like seL4…
Actually if you use the smm verifier that's been cut down to about 800ms. :) However, most of the theorem provers of today have been built on the philosophy that performance doesn't matter, or at least is secondary to…
Note that this is editorial license on the part of the writer; Buzzard is proposing the use of interactive theorem provers, which only use a small amount of 80's style AI (backtracking search and higher order matching).…
Luckily, this is a solvable problem. A theorem prover is software, so you can apply formal methods to it, and prove that the software performs its stated function. The CakeML project does this, and I'm working on a…
Only if you're an ideal rational agent. Maths is hard.
The naming system is pretty compact but also very standardized and reliable, which is important when organizing more than 10000 theorems. That one breaks down as "re + add + cl + i" for "the REals are CLosed under…
If you ever use another proof assistant, you will find that too much documentation is much better than not enough. You can certainly skip the documentation in the main pages if you get the gist. I think Metamath is most…
It sounds like you are talking about Cantor's theorem, and its proof is here -> http://us.metamath.org/mpeuni/canth.html . The formalization is both short and straightforward, so while you might argue that the axioms of…
Fun fact, there have been 3 soundness bugs in lean 4 so far. (They were all fixed within hours.) I expect we have not yet found them all, but I also do not sleep poorly worried that mathematics will come tumbling down,…
Should I introduce you to https://arxiv.org/abs/2403.14064 ?
If this is your situation, you should absolutely be asking more questions on Zulip. It is really easy to get guidance on how to use mathlib, what things exist and where they are. The issue with stacked casts is mostly…
No, Lean is not suitable for axiomatic investigations, it comes with too much baggage from "classical foundations". As Randall said above, Lean is axiomatically much stronger than NF, and that's even with "no axioms"!…
> Speaking of Miri, is the long term goal to say for certain whether or not a program execution encountered UB? (Which is, of course, different than verifying it before execution at compile time.) That's more than a…
Yes, that is incorrect. If you write `partial def foo : Nat := foo + 1` it will be accepted, but `def foo : Nat := foo + 1` is not. So while lean checks that functions terminate by default, it is possible to define and…
The jargon is a bit confusing sometimes. In Lean, "refl" does a whole lot more than prove x=x. It is of course available if you want to prove x=x, but the real power of "refl" is that it also proves x=y where x and y…
> implementation in C++ rather than a nice functional language for dogfooding To be fair, the main author of Lean has been cloistered for two years writing the next version, Lean 4, which is written in its own (pure…
For those who are more into watching talks on YouTube than reading papers, and are interested in the low level hardware formalization aspect of this project, there is a recording of the ITP 2019 presentation here: "x86…
It does, but only if you state the theorem in a particular way. Let's say that you have a verifier A, that checks theorems in Peano Arithmetic (PA). Inside that logic, you can define what a computer is, how it executes,…
(I'm the author of the paper BTW.) Regarding TLA+ and CakeML: TLA+ seems like a good idea, Leslie Lamport talks a lot of sense in most of his papers. I especially recommend "Composition: A Way to Make Proofs Harder"…
Metamath has tactics, but they aren't part of metamath per se; they are part of the tools that you use to write proofs. You don't make the rest of the world run the same proof search you did hundreds of times, finding…
Software gets more complicated, and so bugs become more common. Hardware gets faster, so speed pressures are reduced on software, so it gets more layered and hence slower; and also more complicated. More layers of…
What if your brain is the bottleneck?
It goes without saying that metamath is not designed to be read from the source directly. To be perfectly fair, Coq isn't either; you can kind of get the gist but to really understand what's going on you have to start…
The verification of entire proof libraries (like the entire Coq standard library, or the Isabelle Archive of Formal proofs) usually ranges from hours to days, as do some of the larger computer science projects like seL4…
Actually if you use the smm verifier that's been cut down to about 800ms. :) However, most of the theorem provers of today have been built on the philosophy that performance doesn't matter, or at least is secondary to…
Note that this is editorial license on the part of the writer; Buzzard is proposing the use of interactive theorem provers, which only use a small amount of 80's style AI (backtracking search and higher order matching).…
Luckily, this is a solvable problem. A theorem prover is software, so you can apply formal methods to it, and prove that the software performs its stated function. The CakeML project does this, and I'm working on a…
Only if you're an ideal rational agent. Maths is hard.
The naming system is pretty compact but also very standardized and reliable, which is important when organizing more than 10000 theorems. That one breaks down as "re + add + cl + i" for "the REals are CLosed under…
If you ever use another proof assistant, you will find that too much documentation is much better than not enough. You can certainly skip the documentation in the main pages if you get the gist. I think Metamath is most…
It sounds like you are talking about Cantor's theorem, and its proof is here -> http://us.metamath.org/mpeuni/canth.html . The formalization is both short and straightforward, so while you might argue that the axioms of…