One of the most important things going on right now, that people aren’t paying attention to: Kevin Buzzard is (with others) formalizing the entire undergraduate mathematics curriculum in Lean. (So that all the proofs will be formally verified.)
Missed this when it came out, but apparently Lean was used to formally verify an uncertain section of a proof in some cutting edge work in the first half of 2021:
And it all happened much faster than anyone had imagined. Scholze laid out his challenge to proof-assistant experts in December 2020, and it was taken up by a group of volunteers led by Johan Commelin, a mathematician at the University of Freiburg in Germany. On 5 June — less than six months later — Scholze posted on Buzzard’s blog that the main part of the experiment had succeeded. “I find it absolutely insane that interactive proof assistants are now at the level that, within a very reasonable time span, they can formally verify difficult original research,” Scholze wrote.
Sorry for the stupid question, and I liked the talk and agree it’s a really neat project, but why is it so important? Do you mean important for math, or important for humanity / the future / whatever?
Mostly it just seems significant in the grand scheme of things. Our mathematics is going to become formally verified.
In terms of actual consequences, it’s maybe not so important on its own. But putting a couple pieces together (this, Dan Selsam’s work, GPT), it seems like we’re going to get much better AI-driven automated theorem proving, formal verification, code generation, etc relatively soon.
I’d expect these things to start meaningfully changing how we do programming sometime in the next decade.
Yeah, I get some aesthetic satisfaction from math results being formally verified to be correct. But we could just wait until the AGIs can do it for us… :-P
Yeah, it would be cool and practically important if you could write an English-language specification for a function, then the AI turns it into a complete human-readable formal input-output specification, and then the AI also writes code that provably meets that specification.
I don’t have a good sense for how plausible that is—I’ve never been part of a formally-verified software creation project. Just guessing, but the second part (specification → code) seems like the kind of problem that AIs will solve in the next decade. Whereas the first part (creating a complete formal specification) seems like it would be the kind of thing where maybe the AI proposes something but then the human needs to go back and edit it, because you can’t get every detail right unless you understand the whole system that this function is going to be part of. I dunno though, just guessing.
AI generates test cases for its candidate functions, and computes their results
AI formally analyzes its candidate functions and looks for simple interesting guarantees it can make about their behavior
AI displays its candidate functions to the user, along with a summary of the test results and any guarantees about the input output behavior, and the user selects the one they want (which they can also edit, as necessary)
In this version, you go straight from English to code, which I think might be easier than from English to formal specification, because we have lots of examples of code with comments. (And I’ve seen demos of GPT-3 doing it for simple functions.)
I think some (actually useful) version of the above is probably within reach today, or in the very near future.
One of the most important things going on right now, that people aren’t paying attention to: Kevin Buzzard is (with others) formalizing the entire undergraduate mathematics curriculum in Lean. (So that all the proofs will be formally verified.)
See one of his talks here:
Missed this when it came out, but apparently Lean was used to formally verify an uncertain section of a proof in some cutting edge work in the first half of 2021:
https://www.nature.com/articles/d41586-021-01627-2
Sorry for the stupid question, and I liked the talk and agree it’s a really neat project, but why is it so important? Do you mean important for math, or important for humanity / the future / whatever?
Mostly it just seems significant in the grand scheme of things. Our mathematics is going to become formally verified.
In terms of actual consequences, it’s maybe not so important on its own. But putting a couple pieces together (this, Dan Selsam’s work, GPT), it seems like we’re going to get much better AI-driven automated theorem proving, formal verification, code generation, etc relatively soon.
I’d expect these things to start meaningfully changing how we do programming sometime in the next decade.
Yeah, I get some aesthetic satisfaction from math results being formally verified to be correct. But we could just wait until the AGIs can do it for us… :-P
Yeah, it would be cool and practically important if you could write an English-language specification for a function, then the AI turns it into a complete human-readable formal input-output specification, and then the AI also writes code that provably meets that specification.
I don’t have a good sense for how plausible that is—I’ve never been part of a formally-verified software creation project. Just guessing, but the second part (specification → code) seems like the kind of problem that AIs will solve in the next decade. Whereas the first part (creating a complete formal specification) seems like it would be the kind of thing where maybe the AI proposes something but then the human needs to go back and edit it, because you can’t get every detail right unless you understand the whole system that this function is going to be part of. I dunno though, just guessing.
The workflow I’ve imagined is something like:
human specifies function in English
AI generates several candidate code functions
AI generates test cases for its candidate functions, and computes their results
AI formally analyzes its candidate functions and looks for simple interesting guarantees it can make about their behavior
AI displays its candidate functions to the user, along with a summary of the test results and any guarantees about the input output behavior, and the user selects the one they want (which they can also edit, as necessary)
In this version, you go straight from English to code, which I think might be easier than from English to formal specification, because we have lots of examples of code with comments. (And I’ve seen demos of GPT-3 doing it for simple functions.)
I think some (actually useful) version of the above is probably within reach today, or in the very near future.
Seems reasonable.