Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
1–10 of 140 posts
Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
#2A quick intro from quanta magazine to Kevin Buzzard's work on computer-assisted proof systems
Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
#3I recommend the following post, by the author of the proof, for deeper context. Especially near the end, they talk about some of the things they're trying to accomplish with it in plain(ish) English.
https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-e...
Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
#4The article is interesting, but that lede is incoherent. Many mathematicians accept computer proofs the way chess grand masters accept computer players. Computer “assistants” that generate proofs that humans cannot follow or understand will always be controversial, and the proofs they generate, even though accepted as valid, will always be decorated with an asterisk.
Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
#5The article is interesting, but that lede is incoherent. Many mathematicians accept computer proofs the way chess grand masters accept computer players. Computer “assistants” that generate proofs that humans cannot follow or understand will always be controversial, and the proofs they generate, even though accepted as valid, will always be decorated with an asterisk.
This is a proof assistant, not an automated theorem prover. The user has to supply* the mathematics and the proof checker formally verifies whether or not the steps are correct. It doesn’t have any creativity (that’s up to the mathematician).
*I should have clarified there is some proof generation, see the comment below by opnitro, but I meant the meat and potatoes of novel non-trivial proofs currently has to be supplied by the user.
Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
#6For more details about the actual proof, see: 'Blueprint for the Liquid Tensor Experiment'
Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
#7Interesting choice of the proof assistant though - some specific parts of the Lean's core are not completely decidable, moreover the upcoming Lean 4 version is incompatible with many libraries and proofs written for Lean 3. See also the discussion[1] if the Coq is suitable for number theory as quotients are ubiquitous here.
Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
#8The article is interesting, but that lede is incoherent. Many mathematicians accept computer proofs the way chess grand masters accept computer players. Computer “assistants” that generate proofs that humans cannot follow or understand will always be controversial, and the proofs they generate, even though accepted as valid, will always be decorated with an asterisk.
This is a proof assistant, not an automated theorem prover. The user has to supply* the mathematics and the proof checker formally verifies whether or not the steps are correct. It doesn’t have any creativity (that’s up to the mathematician). *I should have clarified there is some proof generation, see the comment below by opnitro, but I meant the meat and potatoes of novel non-trivial proofs currently has to be supp…
Thanks for the clarification.
Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
#9The article is interesting, but that lede is incoherent. Many mathematicians accept computer proofs the way chess grand masters accept computer players. Computer “assistants” that generate proofs that humans cannot follow or understand will always be controversial, and the proofs they generate, even though accepted as valid, will always be decorated with an asterisk.
This is a proof assistant, not an automated theorem prover. The user has to supply* the mathematics and the proof checker formally verifies whether or not the steps are correct. It doesn’t have any creativity (that’s up to the mathematician). *I should have clarified there is some proof generation, see the comment below by opnitro, but I meant the meat and potatoes of novel non-trivial proofs currently has to be supp…
That's not quite true. Many of these proof assistants support some level of automation and proof search. I haven't used Lean specifically, but it's quite common in Coq for projects to write proof search techniques specific to the problem domain and utilize them in their proofs.
Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
#10Interesting choice of the proof assistant though - some specific parts of the Lean's core are not completely decidable, moreover the upcoming Lean 4 version is incompatible with many libraries and proofs written for Lean 3. See also the discussion[1] if the Coq is suitable for number theory as quotients are ubiquitous here. [1] https://github.com/coq/coq/issues/10871
I wasn't aware of Lean not being sound and a quick search didn't come up with anything related to that. Could you link a source?