digama0

9 ms·

1.
by digama0 2y ago
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, because these are inv
2.
by digama0 2y ago
Should I introduce you to https://arxiv.org/abs/2403.14064 ?
3.
by digama0 2y ago
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 solved by the `norm_ca
4.
by digama0 2y ago
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&quot
5.
by digama0 3y ago
> 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 long term goal,
6.
by digama0 4y ago
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 run programs containi
7.
by digama0 5y ago
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 are
8.
by digama0 6y ago
> 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 functional) language.
9.
by digama0 7y ago
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 verification fro
10.
by digama0 7y ago
The fast proof checker I talk about is mm0-c: https://github.com/digama0/mm0/tree/master/mm0-c . It is (deliberately) bare bones, and I'm planning on formalizing approximately the assembly that you
11.
by digama0 7y ago
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, what PA is, wha
12.
by digama0 7y ago
(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" ( https:&
13.
by digama0 7y ago
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 the same pro
14.
by digama0 7y ago
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 abstraction means more thi
15.
by digama0 7y ago
What if your brain is the bottleneck?
16.
by digama0 7y ago
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 up Coq and l
17.
by digama0 7y ago
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 and CakeML. You are
18.
by digama0 7y ago
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 ease of use,
19.
by digama0 7y ago
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). No one in ITP i
20.
by digama0 7y ago
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 bootstrapping theore
21.
by digama0 8y ago
Only if you're an ideal rational agent. Maths is hard.
22.
by digama0 8y ago
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 ADDition, I
23.
by digama0 8y ago
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 suited for a certain
24.
by digama0 8y ago
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