Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

nature.com

Post reply on HN
Print view View original

41–50 of 140 posts

Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

#41

Post by mherrmann »

kevinbuzzard wrote: post #36
sabujp wrote: post #23

"Proof assistants can’t read a maths textbook, they need continuous input from humans, and they can’t decide whether a mathematical statement is interesting or profound — only whether it is correct, Buzzard says. Still, computers might soon be able to point out consequences of the known facts that mathematicians had failed to notice, he adds." we're closer to this than people realize

I agree, but I think my statement is accurate today in 2021. I would love to see funds directed towards this sort of question. The big problem is that at high level so so much is skipped over, and you still sometimes have to struggle to put undergraduate-level mathematics into Lean -- this is why UG maths is such a good test case.

Very nice to see you here Kevin. We never interacted but I do still remember a lecture you gave at Imperial in '06 where you filled in for Prof. Liebeck and started with Lemma 1: "I am not Professor Liebeck" ;-) Thank you for the nice memory and your important work on / with Lean.

Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

#43

Post by deadbeef57 »

est wrote: post #42

is there a simpler version of LEAN suitable for high school student level math? Sympy?

You might enjoy http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game...

It's a game implemented in lean, where you work your way through the basic facts about natural numbers.

Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

#45

Post by Tainnor »

This is going to be an exciting area.

I spent some time previously playing with Coq. It's very powerful, but even proving the simplest undergraduate maths statements (say, about group theory) can prove very challenging. I believe that part of this is that Coq uses different mathematical foundations than traditional mathematics, which mostly uses set theory (ZFC, although most people don't care about the specifics). So it can be hard or unnatural to express something like "subgroup". I don't know if Lean fares better in that respect. Coq documentation is also IMHO almost impossible to understand unless you're already very deeply knowledgeable about the system.

We will probably still need some more iterations, to get more user friendly assistants with better documentation and to get adequate teaching resources etc.

Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

#46

Post by raphlinus »

Tainnor wrote: post #45

This is going to be an exciting area. I spent some time previously playing with Coq. It's very powerful, but even proving the simplest undergraduate maths statements (say, about group theory) can prove very challenging. I believe that part of this is that Coq uses different mathematical foundations than traditional mathematics, which mostly uses set theory (ZFC, although most people don't care about the specifics). S…

Lean's foundations are similar to Coq. I think the ergonomics are a bit better.

Most activity in proof systems is based in type theory these days, but set theoretical systems do exist, of which Metamath is the most mature. That said, Metamath is seriously lacking in automation, so there is an element of tedium involved. That's not because of any fundamental limitations, but I think mostly because people working in the space are more motivated to do things aligned with programming language theory. There was also a talk by John Harrison a few years ago proposing a fusion of HOL and set theory, but I'm not sure there's been much motion since then.

I believe a fully featured proof assistant based in set theory would be a great contribution.

[1]: http://aitp-conference.org/2018/slides/JH.pdf

Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

#47

Post by kmill »

kevinbuzzard wrote: post #33
martincmartin wrote: post #14

Earlier quoted context omitted.

See other comment. It's sound but not decidable.

Basically it turned out that theoretical undecidability did not matter in practice, because Scholze mathematics relies so little on definitional equality. We prove theorems with `simp` not `refl`. Pierre-Marie Pédrot is quoted above as saying that various design decisions are "breaking everything around", but we don't care that our `refl` is slightly broken because it is regarded as quite a low-level tool for the tas…

And in "Lean style", refl proofs are a bit distasteful from a software engineering point of view because they pierce through the API of a mathematical object. (In the language of OOP, it can break encapsulation.)

It tends to be a good idea to give some definition, then prove a bunch of lemmas that characterize the object, and finally forget the definition.

Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

#48

Post by bryan0 »

deadbeef57 wrote: post #28
kungito wrote: post #27

Earlier quoted context omitted.

What's the name of this point? It's really hard to find any progress on this topic regarding Mochizuki other than some popular articles without any content.

See https://www.math.columbia.edu/~woit/wordpress/?p=10560 , which links to a technical write-up by Scholze and Stix about what they think is the issue with Mochizuki's proof. Woit's blogpost also gives a bit more links, including a response by Mochizuki.

The paper which everyone linked to when the discussion was going on now 404s, so here is a new link: https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture...

The point in the proof where scholze and stix show it fails is “IUTT-3, Corollary 3.12”

Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

#49

Post by gwern »

sabujp wrote: post #23

"Proof assistants can’t read a maths textbook, they need continuous input from humans, and they can’t decide whether a mathematical statement is interesting or profound — only whether it is correct, Buzzard says. Still, computers might soon be able to point out consequences of the known facts that mathematicians had failed to notice, he adds." we're closer to this than people realize

It's worth noting that GPT-f already gets a big performance boost from pretraining on Arxiv etc (https://arxiv.org/pdf/2009.03393.pdf#page=7) despite those sources containing next to no Metamath or anything that looks like a raw Metamath proof, just regular natural language & LaTeX discussing math...

Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

#50

Post by civilized »

Barrin92 wrote: post #16

The abiltiy to automate proofs creates some interesting questions about the nature of mathematics. The article remined me of Erdos saying that you "don't need to believe in God, but you do need to believe in the book", 'the book' here being an imagined collection of mathematical proofs that are so simple, clear and beautiful that they immedieately stand out to any mathematician. I don't mind proof assistants as a way…

Automated proofs aren't remotely comparable to Mochizuki's abc stuff. Automated proofs just handle a lot of complicated case by case checking that humans could in principle do, it's just too much work, like counting to a trillion. Automated proof systems are incapable of the brilliant but unreliable intuitive leaps that mathematicians can make.

Mochizuki's stuff is simply a hypercomplicated pile of nonsense unintelligible to the mathematical community.

Post reply on HN