(I have spent a good amount of time hacking the llvm pass pipeline for my personal project so if there was a significant difference I probably would have seen it by now)
You are correct, that was an uneducated guess on my part.
I just glanced at the IR which was different for some attributes (nounwind vs mustprogress norecurse), but the resulting assembly is 100% identical for every optimization level.
Understanding IMO is "developing a correct mental model of a concept".
Some heuristics of correctness:
Feynman: "What I cannot build. I do not understand"
Einstein: "If you can't explain it to a six year old, you don't understand it yourself"
Of course none of this changes anything around the machine generated proofs. The point of the proof is to communicate ideas; formalization and verification is simply a certificate showing that those ideas are worth checking out.
Ideas and correctness depend on each other. You usually start with an idea, and check if it is correct. If not, you adjust the idea until it becomes correct. Once you have a correct idea, you can go looking for more ideas based on this.
Formalisation and (formulating) ideas are not separate things, they are both mathematics. In particular, it is not that one should live in Lean, and the other one in blueprints.
Formalisation and verification are not simply certificates. For example, what language are you using for the formalisation? That influences how you can express your ideas formally. The more beautiful your language, the more the formal counter part can look like the original informal idea. This capability might actually be a way to define what it means for a language to be beautiful, together with simplicity.
I share your fascination with proof assistants and formal verification, but the reality is that I am yet to see an actual mathematician working on frontier research who is excited about formalizing their ideas, or enthusiastic about putting in the actual (additional) work to build the formalization prerequisites to even begin defining the theorem's statement in that (formal) language.
You know what? I agree with you. I have not formalised any of my stuff on abstraction logic [1] for that reason (although that would not be too difficult in Isabelle or Lean), I want to write it down in Practal [2], this becoming possible I see as the first serious milestone for Practal. Eventually, I want Practal to feel more natural than paper, and definitely more natural than LaTeX. That's the goal, and I feel many people now see that this will be possible with AI within the next decade.
>I am yet to see an actual mathematician working on frontier research who is excited about formalizing their ideas
British mathematician Kevin Buzzard has been evangelizing proof assistants since 2017. I'll leave it to you to decide whether he is working on frontier research:
Sure, he is one of biggest advocates for it, and yet he was quite clear that it is not yet possible for him to do his actual research in Lean.
Quoting one of the recent papers (2020):
> With current technology, it would take many person-decades to formalise Scholze’s results. Indeed,
even stating Scholze’s theorems would be an achievement. Before that, one has of course to formalise
the definition of a perfectoid space, and this is what we have done, using the Lean theorem prover.
> more than 1,000,000 lines of Lean 4 code and concluding with a QED.
Usually the point of the proof is not to figure out whether a particular statement is true (which may be of little interest by itself, see Collatz conjecture), but to develop some good ideas _while_ proving that statement. So there's not much value in verified 1mil lines of Lean by itself.
You'd want to study the (Lean) proof hoping to find some kind of new math invented in it or a particular trick worth noticing.
LLM may first develop a proof in natural language, then prove its correctness while autoformalizing it in Lean. Maybe it will be worth something in that case.
No, the point of proofs in mathematics IS to prove a particular statement is true, given certain axioms (accepted truths). Yes, there are numerous benefits beyond demonstrating something is undeniably true, given certain accepted truths, perhaps more “useful” than the proof itself, but math is a method of formal knowledge that doesn’t accept shortcuts.
A lot of mathematicians (myself included) would say that the point of proofs isn’t entirely to know whether or not a statement is true, but that it exists to promote human understanding. In fact, I’d argue that at some level, knowing whether or not a theorem is true can be less important than understanding an argument.
This is why having multiple different proofs is valuable to the math community—because different proofs offer different perspectives and ways of understanding.
Before Church there was Peano, and before Peano there was Grassmann
> It is rather well-known, through Peano's own acknowledgement, that Peano […] made extensive use of Grassmann's work in his development of the axioms. It is not so well-known that Grassmann had essentially the characterization of the set of all integers, now customary in texts of modern algebra, that it forms an ordered integral domain in which each set of positive elements has a least member. […] [Grassmann's book] was probably the first serious and rather successful attempt to put numbers on a more or less axiomatic basis.
What would you suggest as a reference problem (a benchmark of sorts) to try to play with formal methods for someone with just a bit of formal verification background but not in the field of software verification? Can you suggest some helpful materials?
I've come across TLA+ multiple times, but it seems it was more targeted towards distributed systems (Lamport being the creator, that makes sense). Is it correct, that it would be useless in other domains?
I wonder, what is the actual blocker right now? I'd assume that LLMs are still not very good with specifications and verifcation languages? Anyone tried Datalog, TLA+, etc. with LLMs? I suppose that Gemini was specifically trained on Lean. Or at least some IMO-finetuned fork of it. Anyhow, there's probably a large Lean dataset collected somewhere in Deepmind servers, but that's not certification applicable necessarily, I think?
> AI also creates a need to formally verify more software: rather than having humans review AI-generated code, I’d much rather have the AI prove to me that the code it has generated is correct.
At RL stage LLMs could game the training*, proving easier invariants then actually expected (the proof is correct and possibly short - means positive reward). It would take additional care it to set it up right.
* I mean, if you set it to generate a code AND a proof to it.
LLVM makes it so much easier to build a compiler - it's not even funny. Whenever I use it, I feel like I'm just arranging some rocks on a top of a pyramid.
What language do you use parser combinators in, and what kind of grammar do you parse usually? Nom was terribly verbose and unergonomic even by Rust's standards. Haskell's Megaparsec/Parsec is good but yeah, it's Haskell, you need to handle multiple monads (Parser itself is monadic, then your AST state, and maybe some error handling) at once and that's where I got confused. But I appreciated the elegance.
I experimented with PCs in Haskell and Rust (nom), then moved on to parser generators in Rust (pest.rs), Ocaml (Menhir), Haskell (Happy) and finally ended up with python's Lark - the speed of experimenting with different syntax/grammars is just insane.
Parser combinators is more of a concept than a library. You could make your own supporting the stuff you need. I like writing programs in languages I don't know or I barely know. I usually just take one of the popular libraries in any given language.
For Rust I used Nom and I didn't mind it all that much although I noticed it's quite baroque. If I had more to write I'd probably make some wrappers or macros of my own for most commonly used Nom snippets.
I've used tree-sitter for generating my parsers in Rust, and just working with the untyped syntax tree it generates, and gives you error-tolerance for free. It's a bit of a setup at first tho, requiring an extra crate for the generated parser, but editing it from there saves so much time.
What do you mean exactly by "error-tolerance"? Is it like, each node is wrapped into a result type, that you have to match against each time you visit it, even though you know for a fact, that it is not empty or something like that?
I suppose that one of the pros of using tree-sitter is its portability? For example, I could define my grammar to both parse my code and to do proper syntax highlighting in the browser with the same library and same grammar? Is that correct? Also it is used in neovim extensively to define syntax for a languages? Otherwise it would have taken to slightly modify the grammar.
Oh nono, with tree-sitter, you get an untyped syntax tree. That means, you have a Cursor object to walk the tree, which creates Node objects as you traverse, that have a "kind" (name of the tree-sitter node), span, and children. (I recommend using the rust tree-sitter bindings itself, not the rust wrapper rust-sitter).
Yes, portability like that is a huge benefit, though I personally utilized it for that yet. I just use it as an error-tolerant frontend to my compiler.
As to how errors are reported, tree-sitter creates an ERROR or MISSING node when a particular subtree has invalid syntax. I've found that it never leaves a node in an invalid state, (so never would it create a binaryop(LeftNode(...), Op, ERROR) if RightNode is not optional. Instead it would create an ERROR for binaryop too. This allows you to safely unwrap known fields. ERROR nodes only really bunch up in repeat() and optional()s where you would implicity handle them.
Error tolerance in this context means the parser produces a walkable AST even if the input code is syntactically invalid, instead of just throwing/reporting the error. It’s useful for IDEs, where the code is often in an invalid state as the developer is typing, but you still want to be able to report diagnostics on whatever parts of the code are syntactically valid.
IMO type checking is the best thing to happen to Python in recent memory and eliminates a whole class of developer errors. Getting linters to pass 100% also scratches a weird itch for me, like collecting items in a video game haha.
I do like working with memory, seeing a custom slab allocator used in production code was one of the more interesting aspects of the little experience I had with c++, but always having to be "on guard" so as to not shoot myself in the foot with pointer manipulation was kind of exhausting.
That "itch" is exactly what I meant, lol! And I agree!
I'd definitely give Rust a try. Playing around with types and traits until they click is genuinely addictive - it feels like solving a puzzle or something
reply