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

101–110 of 140 posts

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

#101

Post by hopfenspergerj »

dr_kiszonka wrote: post #92
gigatexal wrote: post #22

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 a…

I know nothing about topology. If you have time, could you please explain this sentence? "For example, any triangle is topologically equivalent to any other triangle — or even to a circle — but not to a straight line." Is it because triangles and circles are "2D" and lines aren't?

If you remove a point from a line, it breaks into two pieces.

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

#102

Post by est »

Tainnor wrote: post #44
est wrote: post #42

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

sympy is not a proof assistant, but a symbolic computer algebra system

Well I'd say it's enough to automatically solve many high-school level problems, automatically. Like a poor man's Mathematica or WolframAlpha.

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

#103

Post by contrarian_5 »

i love the time that we live in. people talk about there being a glut of podcasts, but i can type "Peter Scholze" into youtube and there is a full hour-long interview with him hosted by another mathematician. you can see her channel is very new and almost certainly a part of this latest wave of pandemic podcasters. its so great to take an interest in a random person from a nature article and be able to immediately get a visceral idea of who he is and what hes about.

https://www.youtube.com/watch?v=HYZ3reRcVi8

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

#104

Post by davnn »

civilized wrote: post #50
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 unintelli…

> Automated proof systems are incapable of the brilliant but unreliable intuitive leaps that mathematicians can make.

I would add current automated proof systems. IMHO we are just at the beginning that mathematicians realize the usefulness of technology, which was basically neglected ever since.

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

#105

Post by bpcpdx »

This kinda gives me chills because I can't help but think of Warhammer 40k.

Essentially our civilization progressed to the point where computers started to take more of a role in new discoveries much like in the real world. As computers got more powerfull and AI developed naturally scientific advancement sped up. But there came a point when the science and math became too advanced for humans to even comprehend, so computers did it. Then there came a point when things were so advanced that even scientists couldn't even ask the right questions so an AI intermediate would have to be used.

Then things get weird and you have the 40k universe.

Anyways I know I probably butchered it a little but that's the gist of it and I can totally see things progressing in the real world up to the point where things get weird in 40k.

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

#106

Post by astrange »

gwern wrote: post #49
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...

How well does text extraction from a PDF work? I almost never try it but thought there were random spaces in the output and such things.

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

#107

Post by QuesnayJr »

dr_kiszonka wrote: post #92
gigatexal wrote: post #22

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 a…

I know nothing about topology. If you have time, could you please explain this sentence? "For example, any triangle is topologically equivalent to any other triangle — or even to a circle — but not to a straight line." Is it because triangles and circles are "2D" and lines aren't?

You can give a function that maps the points of the triangle to the points of the circle in such a way that this function is continuous. (Continuous basically means "no jumps".)

You can give this function explicitly. Let's assume that the triangle is drawn on a piece of paper with an x and y axis, such that the intersection of the axes (the origin) is inside the triangle. For each point on the triangle, draw a line from the origin to the point. Take the angle between that line and the x-axis. Use that angle to map it onto a circle.

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

#108

Post by runeks »

> But systems known as proof assistants go deeper. The user enters statements into the system to teach it the definition of a mathematical concept — an object — based on simpler objects that the machine already knows about. A statement can also just refer to known objects, and the proof assistant will answer whether the fact is ‘obviously’ true or false based on its current knowledge.

As far as I can see this is just programming. How is this different from writing in Java

  int i = “hello”
and seeing that the Java compiler rejects this “thesis”?

Of course, we need more complex types than “int” and “String”, but in principle it’s the same.

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

#109

Post by fspeech »

runeks wrote: post #108

> But systems known as proof assistants go deeper. The user enters statements into the system to teach it the definition of a mathematical concept — an object — based on simpler objects that the machine already knows about. A statement can also just refer to known objects, and the proof assistant will answer whether the fact is ‘obviously’ true or false based on its current knowledge. As far as I can see this is just…

Yes and the isomorphism is known as Curry-Howard Correspondence https://en.wikipedia.org/wiki/Curry-Howard_correspondence

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

#110

Post by robinzfc »

raphlinus wrote: post #46
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 th…

It depends on what you mean by "fully featured" but Isabelle supports ZF logic [1] and also you can do ZFC in Isabelle/HOL [2]. And, of course there is Mizar [3].

[1] https://isabelle.in.tum.de/dist/library/ZF/ZF/index.html

[2] https://www.isa-afp.org/entries/ZFC_in_HOL.html

[3] http://mizar.org/

Post reply on HN