Given all the BS info that apparently underlies at least some AI, I hope that someone slips a line of code into that program stating that Side-Side-Angle works for determining congruency.
It does!
Angle-side-side is the broken one.
Hmmm Perhaps that's why I, who generally was very good at math, got only a B in 10th grade Geometry.
I think there's two major caveats here:
1. These specific kind of geometry problems are "decidable" in the sense that there exists an algorithm which can determine which are true and which are false. This is unusual, for example already natural numbers don't have that property.
2. The output here is human-readable, but it's hardly what a human-written proof would look like.
That said, I think odds are good that within my lifetime AI more-or-less makes the research side of my job obsolete. At the end of the day, math isn't actually harder than Chess or Go, so once computers can be taught the rules they'll be very good at proving things, and the huge huge progress in proof formalization means that they're getting very close to being able to teach the computers the rules.. Maybe there's still a role for humans in terms of producing good *questions*, but that'd be a job for a much smaller group of people anyway and would quickly mean the bulk of the profession is unnecessary. But this particular story hasn't really affected my thinking on this very much.
That said, I think odds are good that within my lifetime AI more-or-less makes the research side of my job obsolete.
That's remarkable; I wouldn't have guessed that.
In my job, instead of writing a bunch of buggy code, I can now get AI to write a bunch of buggy code. Most of the work is still in finding the bugs, though.
I mean I'm by nature a pessimist who is drawn to doom-scenarios, so take that viewpoint with a grain of salt. The two big things that have me in this frame of mind are the enormous leaps and bounds that Lean/mathlib have made in the past few years on proof formalization, and neural nets in Chess and Go Engines (AlphaZero and its consequences) which changed things from "some games with simple rules computers are great at, but some they're terrible at, and even in the ones they're great at they're still worse in certain specific ways" to "computers are just much much better than humans at all games, and you don't even need to input human wisdom at any stage of the process." Math is not the same thing as winning at games, but it's awful similar.
Like even 5-10 years ago when computers were way way better than people at Chess, they still didn't really understand openings and you had to take their early move recommendations with a large grain of salt. Now they're just right, and opening preparation is just finding a move that hasn't been played before, memorizing what the computer tells you to do, and hoping your opponent hasn't memorized it. And then it's a one-time try because after they game they'll just go home and memorize what the computer says.
I can play any computer in the world to a draw in tic-tac-toe. I'm sure a bit more work will get someone there in chess.
Maybe there's still a role for humans in terms of producing good *questions*, but that'd be a job for a much smaller group of people anyway and would quickly mean the bulk of the profession is unnecessary.
I think there'd be a need for a large group of referees, essentially, to verify that computers aren't veering into the realm of 6-fingered hands or anything. And possibly, when the computers start making giant leaps and bounds, to translate it into smaller bite size pieces for whoever is left reading this stuff.
For Candyland, the refs need to check that I don't move the skip card to the top of the deck.
I have become very good at Civ 6, but the computer still usually wins.
That's why I always play Civ V. I'm still getting used to the expansion packs. It takes forever to play a game with them.
11: This is why proof assistants are so key to the whole thing, in the past 5 years we now have a large serious project which does computer verified proofs in a language called Lean that is advanced to the point where they've recently verified two major recent results by Fields medalists, and one of their major goals is a completely computer verified proof of Fermat's Last Theorem. If you can produce proofs in Lean (rather than in natural language) then there's just no issue at all around hallucinations, we know for sure that the proofs are right because they're completely formally verified by Lean.
When computers are cranking out math that no one understands and no one needs to verify, and we haven't even applied the vast majority of the math we have currently, what's the point?
Unfoggetarian @ 7: Um, I've never used Lean, but IIUC it's a "proof assistant", e..g like Coq ? And ... I know about Coq (wrote V5.10). When you formalize a proof in Coq (and, I presume, in Lean) you're not actually getting much mechanical assist. This is by great contrast to systems like ACL2 and the provers used to verify hardware (like, every CPU/FPU/GPU that any of us use) which use enormous and recent advances in "SAT solver" to perform verification.
I wouldn't draw any conclusions about AI from the fact that people formalize stuff in Coq. I mean, have you ever heard of MIZAR? It was a resolution-based proof system developed (IIRC) in Poland behind the Iron Curtain. Yeah: really old. But hey, in the Warsaw Pact there wasn't much for mathematicians to do, eh? So they formalized ENORMOUS BODIES of mathematics in Mizar. All machine-checked proofs. But resolution only gets you so far, which .... isn't very. Again, not much to draw for what AI can or cannot do.
This latest stuff is interesting, in that you might say it's throwing out likely intermediate steps further forward than is immediately derivable from what it already knows, and that maybe helps it make progress. It's an interesting use of AI to augment a symbolic deduction system. Or, an interesting use of a symbolic deduction system to augment an AI.
Unfoggetarian @ 7: A little more. I hope it's obvious that MIZAR also has the property that once a "proof" is completed, it is completely machine-checkable. Just as in LEAN and Coq. And HOL, Isabelle, and a host of other "foundational formal proof systems".
What's different about Lean/mathlib is not the computer side but the human side. A large team of mathematicians has been working on it to get to the point where it is genuinely practical to use in a timely fashion. I think it's developed well past Mizar at this point in terms of how much mathematics is already formalized, and certainly completely dwarfs the others you mentioned. Yes this is something people have been trying to do for decades, but only in the past 5-10 years has it gotten a critical mass where it's become of interest to a large number "ordinary mathematicians" (not working in logic, foundations, CS, etc.).
Here's two articles on the big recent splashy things that have happened (and note that they involve the two greatest active mathematicians in the world):
https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/
https://www.quantamagazine.org/a-team-of-math-proves-a-critical-link-between-addition-and-sets-20231206/
20: there's a big difference, though, between:
1. a large library of mathematics developed using a system
and 2. a powerful automated assistant that is able to prove many things itself without human guidance
Of course, #2 can help achieve #1. But not the other way around. And as far as I know, Lean doesn't have #2.
Proof-systems based on the Calculus of Inductive Constructions can be remarkably powerful in the hands of gifted mathematicians, b/c they allow the formulation of very powerful "induction principles" (hence the name "Inductive Constructions"). These can vastly simplify what would otherwise be very tedious and laborious proofs. But it's still up to the human to find those induction principles. Perhaps you know better, and can point at the automated proof techniques that are used in Lean? Does it use Knuth-Bendix? any BDD or other SAT-solver approaches ? In the last decade-or-two there have been tremendous advances in the field of automated proof systems -- systems that require little human input to prove theorems or verify mathematical formulae; as far as I know, systems such as Coq and Lean have adopted nearly none of those advances.
I don't disagree with that, my point is that progress on 1 has made 2 easier, and it feels to me (and this is purely subjective) that we're nearing the point where 2 will be somewhat similar to winning at games with defined rules and computers are very very good at that now.
It sounds to me like math is basically folk art now.
Now they're just right, and opening preparation is just finding a move that hasn't been played before, memorizing what the computer tells you to do, and hoping your opponent hasn't memorized it. And then it's a one-time try because after they game they'll just go home and memorize what the computer says.
This is so interesting to me (about chess). My kid is really into cubing and it surprises me that there doesn't appear to be any deducing involved. All speed cube solving is (from what I understand) pattern recognition and then applying memorized solutions. When I tell him he cannot look at an algorithm (for the bigger cubes) and he should play with it and try to figure it out, he has no interest.
I practice a sort of manually-electronically-assisted Wordle. Every time I play, I use the same first word, then when I'm done look at the after-action report to see what Wordlebot recommends as the optimal second word given that information. I then store that in a spreadsheet accompanying the green/yellow/gray pattern the first word got so I can look it up and use it the second time the pattern recurs. (I don't do this with the third word though.)
16 et seq: So, how much does all this help you build a hydrogen bomb?
25: So are you going back and changing everything, now that you're supposed to start with TROPE instead of LEAST?
27: I thought the change was from SLATE to TRACE. But yes, I made a new tab and am repopulating the rows day by day.
My thing tells me TROPE! Which of us is getting lied to?!
Is that a Euler in your pocket or are you just glad to see me?
Well, theoretically, if the robots could do everything we could all enjoy tremendous leisure. The problem is that that's not how it works in America.
Surely the mathematicians will enjoy tremendous leisure.
I have a truly novel demonstration of this proposition that the human mind is too small to contain.
Any chance that people can stop invoking Quanta articles as evidence that hype is justified, rather than a manifestation of the hype?
(Grumpy pure mathematician, blowing the cobwebs off this username/id)
I tend to agree with https://garymarcus.substack.com/p/sorry-but-funsearch-probably-isnt although GM clearly has an axe to grind
#17: for some of us, the point of research/scholarship in mathematics is to increase understanding of what has been done or defined, not increase the amount of *stuff* out there in the world. However, I admit that's far from universal even in my own tribe.
OT: I just learned that the "none pizza with left beef" guy went on to create Young Sheldon. Which shows the sophomore curse is real.
This is a good example of a morning where I can't post until lunchtime.
But no worries. I have abundant excerpts from your first civil war.