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

111–120 of 140 posts

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

#111

Post by zant »

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…

Yeah you can say that. You can also say that Machine Learning is just programming. Or in a similar way you can also say that First Order Logic is just programming.

However, the cool thing about programming is that it lets us represent a lot of different things. In this case you're representing the construction and interaction of mathematical objects, with a language that targets a specific proof management system to verify this constructions.

But yes, it is "just programming", and some functional languages even support proofs to some extent like Scala or Agda.

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

#112

Post by zant »

Ericson2314 wrote: post #58
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…

On the contrary proof assistants help one systematize and organize existing concepts. They are a great way to revise the basic curriculum and revolutize pedagogy. They make the creative process of defining new mathematical objects more accessible, and easier to motivate via unlocking more code reuse. They are a great way to revise the basic curriculum and revolutize pedagogy.

I strongly agree on this one. As a programmer and someone who's always been interested in mathematics, having a way to check proofs without relying on trust of my own logic or a third agent, but solely on a prover like Lean or Coq is a really big difference.

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

#113

Post by creata »

Tainnor wrote: post #63
zozbot234 wrote: post #59

Earlier quoted context omitted.

ZFC was only ever developed as a proof of concept, not as a practical foundation for formal math. Structural set theories, type theories or category-based foundations are actually a lot easier to work with, and otherwise quite equivalent in power.

This is missing the point. Modern mathematics textbooks, especially undergratuate ones, are written with set theoretic foundations. It requires a lot of effort to reformulate all of mathematics into equivalent formulations. That makes it harder to get buy-in from many working mathematicians, and it also makes the subject less approachable for, say, undergraduates.

> Modern mathematics textbooks, especially undergratuate ones, are written with set theoretic foundations.

Yes, but only the foundations. A math undergrad doesn't actually care whether an ordered pair (a, b) is encoded as {{a},{a,b}} or as an instance of the product type, and they don't care whether the natural number 2 is encoded as the set {{},{{}}} or as a value S(S(Z)) of the inductive type of the natural numbers. Although if pressured to choose, I bet they'd prefer the latter, since it gets a lot closer to how everyone thinks of "ordered pairs" and "natural numbers".

Since mathematicians always work with higher-level abstractions anyway, I don't think the fact that the very lowest layer of these abstractions is set theory actually gets in the way of formalization efforts.

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

#114

Post by throwaway81523 »

kevinbuzzard wrote: post #39
GPerson wrote: post #32

Earlier quoted context omitted.

Why do you say this?

I'm not quite sure what you're asking about. I'm saying that we can't yet take the Wiles and Taylor-Wiles proof of Fermat's Last Theorem, feed it into a machine, and get a Lean proof of Fermat's Last Theorem.

I remember asking Bob Solovay whether he thought Wiles' proof of FLT was within reach of formalization and he said something like: it is probably 20 years away. It may have been 20 years since I asked him that, and seeing this recent work with Lean makes me think FLT might also be doable, which would make Solovay's guess just about spot on.

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

#115

Post by foooobar »

Jweb_Guru wrote: post #98
bryan0 wrote: post #86

Earlier quoted context omitted.

Thanks for the explanation. Is the defeq undecidability a bug of Lean that should be fixed in the future? Or is it an intentional design decision for it to function properly for other types of proofs?

I am quite confident that the developers of lean consider it a feature (or at least, not a bug). Though I'm also not sure why they are building on a complex metatheory like CiC if they are willing to accept undecidable typechecking since you can simplify a lot of things if you give that up.

What simplifications do you have in mind?

I think one of the reasons is that Lean's approximation of defeq still works well enough in practice. As mentioned by others, you never really run into the kind of counter examples that break theoretical properties, but instead into examples where checking defeq is inacceptably slow, which remains an issue even when defeq is decidable.

From my understanding CiC is used because it allows using a unified language for proofs, specifications, programs and types, which greatly simplifies the system. For example, in Lean 4, more or less the entire system is built on the same core term language: Proofs, propositions / specifications, programs, tactics (i.e. meta programs), the output of tactics and even Lean 4 itself are all written in that same language, even if they don't always use the same method of computation. In my eyes, for the purposes of writing and checking proofs, CiC is quite complex; but if you want to capture all of the above and have them all checked by the same kernel, CiC seems like a fairly minimal metatheory to do so, even with undecidable type checking.

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

#116

Post by hangsi »

astrange wrote: post #106
gwern wrote: post #49

Earlier quoted context omitted.

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.

A fair summary would be "often very well, but not always". A good exmaple would be the S2ORC dataset [0]: a dataset of full parses of scientific PDFs. In their paper, the authors write about the difficulties of getting the parsers to work reliably, and how having multiple published versions of a PDF was helpful for when the PDF parser fails on the first one.

[0] https://allenai.org/data/s2orc

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

#117

Post by mkl »

est wrote: post #102
Tainnor wrote: post #44

Earlier quoted context omitted.

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.

Yes, but that's a totally different category of problem from what proof assistants do.

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

#118

Post by rakhodorkovsky »

deadbeef57 wrote: post #55
wolverine876 wrote: post #54

Earlier quoted context omitted.

Thanks for sharing your expertise. Would you be open to sharing your background? Obviously it's not required, but it would help contextualize what you're saying for the interested non-mathematician; otherwise we're kinda stuck with 'some guy on the Internet said ...' syndrome. :)

Sure, I just created an account a couple of days ago, and my favourite username was already taken :oops: I'm Johan Commelin, https://math.commelin.net/

clicked on the private key link; haven't laughed this much in days

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

#119

Post by kevinbuzzard »

bryan0 wrote: post #86
digama0 wrote: post #60

Earlier quoted context omitted.

The jargon is a bit confusing sometimes. In Lean, "refl" does a whole lot more than prove x=x. It is of course available if you want to prove x=x, but the real power of "refl" is that it also proves x=y where x and y are definitionally equal. Or at least that's the idea; it turns out that lean's definitional equality relation is not decidable so sometimes it will fail to work even when x and y are defeq, and this is…

Thanks for the explanation. Is the defeq undecidability a bug of Lean that should be fixed in the future? Or is it an intentional design decision for it to function properly for other types of proofs?

Defeq undecidability is a feature of Lean in the sense that it is a conscious design decision. As we have seen both in this thread and in other places, this design decision puts off some people interested in the foundations of type theory from working with Lean. However it turns out that for people interested other kinds of questions (e.g. the mathematics of Scholze), defeq undecidability is of no relevance at all.

Here's an analogue. It's like saying "Goedel proved that maths was undecidable therefore maths is unusable and you shouldn't prove theorems". The point is that Goedel's observation is of no practical relevance to a modern number theorist and does not provide any kind of obstruction in practice to the kind of things that number theorists think about.

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

#120

Post by andrepd »

Tainnor wrote: post #63
zozbot234 wrote: post #59

Earlier quoted context omitted.

ZFC was only ever developed as a proof of concept, not as a practical foundation for formal math. Structural set theories, type theories or category-based foundations are actually a lot easier to work with, and otherwise quite equivalent in power.

This is missing the point. Modern mathematics textbooks, especially undergratuate ones, are written with set theoretic foundations. It requires a lot of effort to reformulate all of mathematics into equivalent formulations. That makes it harder to get buy-in from many working mathematicians, and it also makes the subject less approachable for, say, undergraduates.

Not quite. You're conflating two things: using set theory to talk about sets (what undergraduate math textbooks do) and using set theory to talk about everything (what ZFC foundations does).
Post reply on HN