21–30 of 216 posts
Earlier quoted context omitted.
Yes. In fact, Lean is a compiler and type checkers are theorem provers (by the Curry-Howard correspondence). Proofs are programs!
And Mathematics is Computer Science. Took me most of a lifetime to realize this.
Earlier quoted context omitted.
> consider getting mathematics written down properly, i.e. in a formal system This was already tried, and failed (Hilbert). In the aftermath of the failure we learned that mathematics cannot be completely formalized. So this points to a fundamental problem with using AI to do math.
> This was already tried, and failed (Hilbert) Who likely underestimated how hard it would be. And who didn't have a 2024 computer on hand.
This hurts my engineer-brain. Just a reminder than the gap between us and mathematicians is about the same as the gap between us and everybody else (edit: in terms of math skills), just in the other direction, haha. Oh well, hopefully when they get the machines to solve math, they’ll still want them to run a couple percents faster every year.
[flagged]
Past researcher in pure math here. The big problem is that mathematicians are notorious for not providing self-contained proofs of anything because there is no incentive to do so and authors sometimes even seem proud to "skip the details". What actually ends up happening is that if you want a rigorous proof that can be followed theoretically by every logical step, you actually need an expert to fill in a bunch of gaps that simply can't easily be found in the literature. It's only when such a person writes a book explaining everything that it might be possible, and sometimes not even then.
The truth is, a lot of modern math is on shaky ground when it comes to stuff written down.
Earlier quoted context omitted.
Yes. In fact, Lean is a compiler and type checkers are theorem provers (by the Curry-Howard correspondence). Proofs are programs!
And Mathematics is Computer Science. Took me most of a lifetime to realize this.
Earlier quoted context omitted.
> This was already tried, and failed (Hilbert) Who likely underestimated how hard it would be. And who didn't have a 2024 computer on hand.
The reason Hilbert failed is because it’s mathematically impossible (Gödels incompleteness theorem).
I guess the Lean devs can all pack and go home then. Also: how could they possibly miss Gödel's theorem, how careless of them.
Well, I never was much of a number theorist. I never did come to understand the basic definitions behind the BSD conjecture. Number theory is so old, so deep, that writing a PhD on the topic is the step one takes to become a novice. Where I say that I didn't understand the definitions, I certainly knew them and understood the notation. But there's a depth of intuition that I never arrived at. So the uproar of experts, angry that I had the audacity to hope for a counterexample, left me more curious than shaken: what do they see, that they cannot yet put words to?
I am delighted by these advances in formalism. It makes the field feel infinitely more approachable, as I was a programmer long before I called myself a mathematician, and programming is still my "native tongue." To the engineers despairing at this story, take it from me: this article shows that our anxiety at the perceived lack of formalism is justified, but we must remember that anxiety is a feeling -- and the proper response to that feeling is curiosity, not avoidance.
Okay, for some decades, I've read, written, taught, applied, and published, in total, quite a lot of math. Got a Ph.D. in applied math.
Yes, there are problems in writing math, that is, some math is poorly written.
But, some math is quite nicely written. (1) Of course, at least define every symbol before using it. (2) It helps to motivate some math before presenting it. (3) Sometimes intuitive statments can help.
For more, carefully reading some well-written math can help learning how to write math well:
Paul R.\ Halmos, {\it Finite-Dimensional Vector Spaces, Second Edition,\/} D.\ Van Nostrand Company, Inc., Princeton, New Jersey, 1958.\ \
R.\ Creighton Buck, {\it Advanced Calculus,\/} McGraw-Hill, New York, 1956.\ \
Tom M.\ Apostol, {\it Mathematical Analysis: Second Edition,\/} ISBN 0-201-00288-4, Addison-Wesley, Reading, Massachusetts, 1974.\ \
H.\ L.\ Royden, {\it Real Analysis: Second Edition,\/} Macmillan, New York, 1971.\ \
Walter Rudin, {\it Real and Complex Analysis,\/} ISBN 07-054232-5, McGraw-Hill, New York, 1966.\ \
Leo Breiman, {\it Probability,\/} ISBN 0-89871-296-3, SIAM, Philadelphia, 1992.\ \
Jacques Neveu, {\it Mathematical Foundations of the Calculus of Probability,\/} Holden-Day, San Francisco, 1965.\ \
Earlier quoted context omitted.
> consider getting mathematics written down properly, i.e. in a formal system This was already tried, and failed (Hilbert). In the aftermath of the failure we learned that mathematics cannot be completely formalized. So this points to a fundamental problem with using AI to do math.
While it's true that mathematics cannot ever be completely formalized, per Gödel's incompleteness theorems, a huge amount of it obviously can, as is demonstrated by the fact that we can write it down in a reasonably rigorous way in a combination of conventional mathematical notation and plain English. Nor is this in any way "a fundamental problem with using AI to do math".
You seem to be imagining that Gödel is just a small problem you can carve off and ignore, but it applies for everything powerful enough to do arithmetic.
Of course we can have the AI muddle along with intuition, but that's not actually an improvement, our mathematicians can already use intuition and they've got a lot more experience.
Much worse, this nonchalant attitude is being taught to PhD students and postdocs both explicitly and implicitly: if you are worried too much, maybe you are not smart enough to understand the arguments/your mathematical sense is not good enough to perceive the essence of the work. If you explain too much, your readers will think you think they are dumb; erase this page from your paper (actual referee feedback).
Also, like Loeffler in the comments, I don't trust the "people have been using crystalline cohomology forever without trouble" argument. The basics are correct, yes, as far as I can tell (because I verified them myself, bearing in mind of course that I am very fallible).
But precisely because of that, large swathes of the theory will be correct. Errors will be rare and circumstantial, and that is part of the problem! It makes them very easy to creep into a line of work and go unnoticed for a long time, especially if the expert community of the area is tiny---as is the case in most sub-areas of research math.