Does anyone know how condensed mathematics would fit into the modern theory of PDEs (which is heavily based on functional analysis)? Perhaps it's a relic of the sort of math Scholze works on, but it looks far too abstract to provide an impetus for people in those fields to embrace it. Topology, on the other hand, is relatively easy to define and work with (though there are some quirks with dual spaces of continuous linear functionals I've seen aesthetic objections to). Or does it "contain" topology in some sense, allowing people to continue working with notions of convergence obtained from norms?
Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
31–40 of 140 posts
Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
#32"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
Why do you say this?
Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
#33Earlier quoted context omitted.
I wasn't aware of Lean not being sound and a quick search didn't come up with anything related to that. Could you link a source?
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 tasks (eg proving theorems of Clausen and Scholze) that we are actually interested in, and I believe our interests contrast quite a lot with the things that Pédrot is interested in.
Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
#34The 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.
If not an asterisk, they’ll just have less impact. A proof generates a fact. The best facts and proofs are useful in that they help other things. You work becomes useful for my work, which may become useful for others.
Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
#35Does anyone know how condensed mathematics would fit into the modern theory of PDEs (which is heavily based on functional analysis)? Perhaps it's a relic of the sort of math Scholze works on, but it looks far too abstract to provide an impetus for people in those fields to embrace it. Topology, on the other hand, is relatively easy to define and work with (though there are some quirks with dual spaces of continuous l…
I think that right now it is not clear why condensed/liquid mathematics would be useful for PDEs. On the other hand, your question
> Or does it "contain" topology in some sense, allowing people to continue working with notions of convergence obtained from norms?
has a positive answer. You can, if you want, swap out topological spaces, and use condensed sets instead, and just continue with life as usual.
At the same time, all of this is in fast paced development, so hopefully we will see some killer apps in the near future. But I expect them more in the direction of Hodge theory and complex analytic geometry.
Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
#36"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.
Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
#37The 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.
Presumably the asterix denotes "actually true"? ;-)
Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
#38The 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?
Lean and the other theorem provers turn mathematical proofs into levels of a computer puzzle game, much like a chess puzzle.
Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
#39"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
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.
Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
#40The 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.
[deleted]