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

21–30 of 140 posts

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

#21

Post by citrusynapse »

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…

Made an account just to share this incredible book that follows Erdos's life & exploits:

https://en.wikipedia.org/wiki/The_Man_Who_Loved_Only_Numbers

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

#22

Post by gigatexal »

For anyone frustrated that the article doesn’t say what specific part of math has the most to gain it’s here:

“ The crucial point of condensed mathematics, according to Scholze and Clausen, is to redefine the concept of topology, one of the cornerstones of modern maths. A lot of the objects that mathematicians study have a topology — a type of structure that determines which of the object’s parts are close together and which aren’t. Topology provides a notion of shape, but one that is more malleable than those of familiar, school-level geometry: in topology, any transformation that does not tear an object apart is admissible. For example, any triangle is topologically equivalent to any other triangle — or even to a circle — but not to a straight line.

Topology plays a crucial part not only in geometry, but also in functional analysis, the study of functions. Functions typically ‘live’ in spaces with an infinite number of dimensions (such as wavefunctions, which are foundational to quantum mechanics). It is also important for number systems called p-adic numbers, which have an exotic, ‘fractal’ topology.”

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

#23

Post by sabujp » 

    "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

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

#24

Post by LudwigNagasena »

ajarmst wrote: post #4

The 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.

I don’t understand the chess analogy. How is it in any way similar?

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

#25

Post by deadbeef57 »

xvilka wrote: post #13
deadbeef57 wrote: post #11

Earlier quoted context omitted.

The claim that Lean's core is not completely sound is FUD. Completely bogus. You might be confused by the fact that Lean's definitional equality is not decidable, but that doesn't mean it isn't sound. Nobody has ever found a proof of `false` so far in Lean 3. The choice for Lean is actually quite natural: (i) it has a large and coherent library of mathematics to build such a project upon. And (ii), it has a substanti…

> You might be confused by the fact that Lean's definitional equality is not decidable, but that doesn't mean it isn't sound. Nobody has ever found a proof of `false` so far in Lean 3. You are right, my bad. Taking my words back on that. A bit more details from the Pierre-Marie Pédrot: > Lean does not escape this limitation, as it defines the equality type inductively as in Coq. Rather, in a mastermind PR campaign, t…

> Lean does not escape this limitation, as it defines the equality type inductively as in Coq. Rather, in a mastermind PR campaign, they successfully convinced non-experts of type theory that they could give them quotient types without breaking everything around.

This is not the first time that I hear someone from the Coq community talk about Lean and its "mastermind PR campaign". To me it comes across in a denigrating way, and frankly I'm a bit sick of it.

Working mathematicians are usually not experts of type theory. Yes. But they aren't stupid either. Why does the Lean community have such a large number of mathematician users? Why did it successfully formalize the main technical result of Peter Scholze's challenge in less than 6 months? Is this all because of a "mastermind PR campaign" selling mathematicians snake oil?

There has been some strong disagreements and even mud slinging between the Coq and Lean communities in the past. But I thought that axe was buried. I would like to move on.

I'm fine with people finding the foundations of Lean ugly, distasteful, improper, or whatever. But please stop the insults.

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

#26

Post by xvilka »

deadbeef57 wrote: post #15
xvilka wrote: post #13

Earlier quoted context omitted.

> You might be confused by the fact that Lean's definitional equality is not decidable, but that doesn't mean it isn't sound. Nobody has ever found a proof of `false` so far in Lean 3. You are right, my bad. Taking my words back on that. A bit more details from the Pierre-Marie Pédrot: > Lean does not escape this limitation, as it defines the equality type inductively as in Coq. Rather, in a mastermind PR campaign, t…

Ok, no worries. I understand that from a theoretical point it's not so nice that defeq is not decidable. But frankly I don't care. Because in practice, I don't know of any example where someone was bitten by this. It only shows up in contrived examples. And even if you have some practical example where lean gets stuck on A = B, it will probably be very easy to find a C so that lean gets unstuck on A = C = B. [Edit, t…

By the way, just for the record, I like many aspects of the new Lean 4 design and wish the project luck. They really aim for better maintainability and user experience. It is nice to see them taking best solutions from other programming languages and frameworks.

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

#27

Post by kungito »

deadbeef57 wrote: post #18
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…

As explained in another comment, there is only very mild proof automation going on in this Lean project. Every non-trivial idea has to be supplied to the computer by a human being. The whole circus around Mochizuki's proof of the abc conjecture was dealt with quite well by the social structure of the mathematical community. Many people looked at the proof. Many people got stuck. Several experts got stuck at exactly t…

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.

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

#28

Post by deadbeef57 »

kungito wrote: post #27
deadbeef57 wrote: post #18

Earlier quoted context omitted.

As explained in another comment, there is only very mild proof automation going on in this Lean project. Every non-trivial idea has to be supplied to the computer by a human being. The whole circus around Mochizuki's proof of the abc conjecture was dealt with quite well by the social structure of the mathematical community. Many people looked at the proof. Many people got stuck. Several experts got stuck at exactly t…

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.

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

#29

Post by inigojonesguy »

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…

[flagged]
Post reply on HN