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

131–140 of 140 posts

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

#131

Post by deadbeef57 »

alimw wrote: post #81
deadbeef57 wrote: post #55

Earlier quoted context omitted.

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/

Hi! Imagine for a moment that your next project required you to develop a lot of functional analysis and PDE theory in Lean. Would you be tempted to build that on top of what you've done (or will have done) with condensed sets?

Right now, I think I would go for that classical approach, simply because there is more supporting material for that in the library, and there are more people who understand that approach and can help contributing. (I'm talking specifically about functional analysis and PDEs here.)

On the other hand, it should be a lot of fun to see if we can formalize the new proof by Clausen--Scholze of Serre duality. Using their machinery, the proof should simplify a lot. But this requires building complex analytic manifolds on top of condensed mathematics. So we would first need to set up those foundations.

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

#132

Post by foooobar »

Jweb_Guru wrote: post #125
foooobar wrote: post #115

Earlier quoted context omitted.

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

For example, if you are willing to accept undecidable typechecking, you can define inductive types in a much simpler theory (inductive types and dependent pattern matching are by far the most complex parts of CiC): https://homepage.cs.uiowa.edu/~astump/papers/from-realizabil... . There are a few other examples but this is the one that immediately sprung to mind. The complexity of CiC is very much about decidable type…

Thanks! But does that not already answer your question as to why Lean would use CIC and not a simpler metatheory?

That particular paper is from 2016 and the type theory presented there is still lacking a number of features from CIC, with those particular extensions being listed as further research. Work on Lean started in 2013 and the kernel in particular has not been touched in a long time for good reason. Around that time, CIC was already battle-proven with there being popular and well-tested reference implementations to learn from. Since then, all the fancy work has been done on the system surrounding the kernel.

I believe one of the goals at the start was that the kernel should be sufficiently simple and small so that it is easy to ensure that the kernel is correct. Despite the apparent redundant complexity that you suggest, the implementation still seems to be sufficiently simple to reach this goal, as no proof of false that was a result of a kernel bug has been reported yet. CIC being well-tested surely also contributed to that.

Another reason is that, as I understand it, it was not always obvious that Lean would break decidability of defeq. Afaik proof irrelevance was only baked in with Lean 3, while it was an option before that. By that point I don't see much of a reason to rewrite an entire kernel that has worked fine so far.

I also vaguely remember that there were arguments related to performance in favor of the current system (e.g. versus W-types), but I don't really understand these things well enough to make that point with confidence :)

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

#133

Post by Jweb_Guru »

kevinbuzzard wrote: post #130
Jweb_Guru wrote: post #128

Earlier quoted context omitted.

That's currently an open research question, but the answer most likely is that the ergonomics could be made just as good, considering that elaboration of metavariables, typeclass instances, etc. already uses possibly-undecidable algorithms distinct from those used in the kernel in just about every proof assistant I'm familiar with (Lean included). In terms of stuff that do go more or less directly through the kernel,…

The fact remains though that Lean 3 worked well enough to do Scholze level mathematics. I never quite know what to make of people saying "if the designers had done it in some other way, it would have been better". Of course if someone comes along doing it another way, and then they go on to also achieve Scholze level mathematics, then I will be all ears.

That's a very strange line of argument. Many great programs have been written in C. That doesn't mean that there is no way to improve on C. Perhaps to even the playing field, this hypothetical competitor should be given the resources of Microsoft Research as well :)

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

#134

Post by Jweb_Guru »

Ericson2314 wrote: post #129
Jweb_Guru wrote: post #96

Earlier quoted context omitted.

That's a nice idea but it tends to fall flat when you can't actually construct an explicit function exhibiting the homomorphism in question (which does happen from time to time). A lot of equivalences in areas like group theory only hold classically.

Your concerns make sense in general, but I have hard time understanding them for would-be subgroups. I would think the "explicit function" would be the easy part. The hard pat is annoyance of finding a "syntactic" representation of the subgroup and proving it's a group (closed) in its own right. In any event, Lean's reputation is that it goes the extra mile for "regular" mathematicians. It probably has something nice…

Nope, proving something is a group doesn't usually run into foundational concerns (at least if you use setoid equality). But finding a function exhibiting a homomorphism can unless you use a functional relation instead (but then you lose most of the nice benefits of using this version of the definition in the first place).

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

#135

Post by foooobar »

Jweb_Guru wrote: post #133
kevinbuzzard wrote: post #130

Earlier quoted context omitted.

The fact remains though that Lean 3 worked well enough to do Scholze level mathematics. I never quite know what to make of people saying "if the designers had done it in some other way, it would have been better". Of course if someone comes along doing it another way, and then they go on to also achieve Scholze level mathematics, then I will be all ears.

That's a very strange line of argument. Many great programs have been written in C. That doesn't mean that there is no way to improve on C. Perhaps to even the playing field, this hypothetical competitor should be given the resources of Microsoft Research as well :)

I think Kevin is asserting that to make strong comparative claims about the quality of either system, it's good to have a large and functionally similar body of work to compare the systems with, not that there is no way to improve on Lean's core :)

MSR funds a single developer. The Lean community consists of at least 30 or so active contributors right now, with many more having contributed in the past. Most folks work in academia. Much of Lean's success is absolutely due to the work of that single developer, but I don't think that the playing field is uneven due to MSR's funding.

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

#136

Post by ninguem2 »

mherrmann wrote: post #41
kevinbuzzard wrote: post #36

Earlier quoted context omitted.

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.

Did he prove the lemma or did he leave it as an exercise :-) ?

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

#137

Post by andrepd »

Tainnor wrote: post #124
andrepd wrote: post #120

Earlier quoted context omitted.

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

In 99% of algebra textbooks you'll see a definition like "if G is a group and H is a subset of G, then we call H a subgroup if it is a group under the same operation." Then, the next thing you see is probably the theorem that "H is a subgroup of G if and only if it is a subset of G and gh^{-1} € H for all g, h € H". That's clearly using the language of set theory to talk about groups . I mean, my argument is not that…

> My sole argument was that you can't currently take any mathematician not particularly interested in logic or proof theory, especially not an undergraduate student, and expect them to encode simple proofs that they understand in Coq without a lot of assistance.

Oh but absolutely, I agree 100%. I consider it the "holy grail" of interactive proof assistants: an assistant that understands mathematics as written by humans in papers, plus is capable of filling in intuitively trivial/boring steps. In other words: an assistant that is usable by someone with training in mathematics but not necessarily requiring training in the tool itself.

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

#138

Post by AtlasBarfed »

The Lean version of the theorem was 10,000s lines of code...

With verifiers like this as a useful tool, I'm guessing in the coming years this LoC will be dwarfed.

I'm a bit surprised a theorem of major complexity reduced to that small a LoC count.

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

#139

Post by AtlasBarfed »

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

Simply having a linked graph of related concepts might show "impact diffs" in theorems.

I recall that the Fermat's proof linked several normally disparate areas to get to the meat of the issue.

Simply tagging those relations to identified sub-fields of study will probably help give guidance to impacts of theories, maybe farm them out to advanced students for quick review.

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

#140

Post by visarga »

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…

> but I worry that maths is drifting into a direction where it turns more into hermeneutics than actual mathematics

Related to the unexplainability of AI. We're just grasping for more than we can hold in our little working memory.

Post reply on HN