Timeline for What are "perfectoid spaces"?
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 14, 2023 at 3:04 | comment | added | Simon Eatwell | @user20948 "I'm not sure whether it helps if more mathematicians start working with formal theorem provers." At least, it would help physicists and engineers to apply mathematical results quickly and without ambiguity, so that correctness can be achieved at a much lower cost. | |
| Dec 4, 2019 at 22:01 | comment | added | user20948 | And I am not that pessimistic. I mean, maybe computers would excel mathematicians in proving theorems. It is even possible that computers would excel mathematicians in building math theories. My question would rather be: how could we take advantage of it if that happens? Just like in the Go case, pro go players can only somehow mimic AI plays, but it is essentially difficult to absorb new ideas and new strategies. I would like to see math as a game of human beings. Even if computers excel us, it is still hard for us to improve our understandings. | |
| Dec 4, 2019 at 21:55 | comment | added | user20948 | I'm not sure whether it helps if more mathematicians start working with formal theorem provers. On one hand, AlphaGo Zero excels professional Go players with rare help from the pro players. On the other hand, mathematicians might not be better at this than computer scientists, I mean, formalizing math is a different art than math. Some are interested out of personal ability. For example, Voevodsky was searching for a better foundation which makes formalization easier - this work per se is hard, and the methods to attack this problem per se are different from those to attack math problems. | |
| Sep 26, 2019 at 20:50 | comment | added | Kevin Buzzard | " surely this is evidence that this kind of proof does not necessarily have an essential place in the business of proving things" -- I dunno. Is that a logical deduction? The five colour theorem doesn't need a computer proof, but I don't think that is evidence that the four colour theorem doesn't need a computer proof. | |
| Sep 25, 2019 at 11:44 | comment | added | Hollis Williams | Hi Kevin, you mention the computer-checked proof of the Kepler conjecture, but I am sure you are aware that this proof was only for dimension 3 or less, whereas the mathematician Viazovska proved the sphere-packing theorem in dimensions 8 and 24 using simple arguments and no long computer calculations, surely this is evidence that this is kind of proof does not necessarily have an essential place in the business of proving things, as Viazovska used clever arguments to prove what took arduous computer calculations to prove only in the Euclidean case. | |
| May 12, 2019 at 10:43 | comment | added | Kevin Buzzard | They are now done! In fact here's an observation which I find sociologically interesting: if I think I have proved a theorem, there comes a point where I begin to start telling other people "I can prove this theorem" -- probably before I have written anything, and perhaps even before I have checked all the final lemmas. But with this perfectoid spaces work, there was no ambiguity. For months it compiled with "a couple of warnings" indicating that, strictly speaking, work still needed to be done. But now the warnings are gone: it was a very clear-cut experience. It now compiles. | |
| May 12, 2019 at 10:02 | comment | added | David Roberts♦ | So they are now defined in Lean? Congratulations! | |
| May 12, 2019 at 7:11 | history | edited | Kevin Buzzard | CC BY-SA 4.0 |
The project is now finished and I updated the post to reflect this.
|
| Aug 8, 2018 at 6:47 | comment | added | David Roberts♦ | I wish I could upvote this answer many times. The news that people are tackling the formalisation of the Stacks Project (not to mention cutting-edge mathematics, like perfectoid spaces) is very exciting. As a point of tribal pride, it's nice to see modern, dependent-type-based proof assistants used for this task, rather than eg Metamath or a ZFC-style system. | |
| Jul 31, 2018 at 11:53 | history | answered | Kevin Buzzard | CC BY-SA 4.0 |