Earlier quoted context omitted.
I’m not sure about this. Anthropic’s AI constructed complex structures on S^6 and wrote a 108 page paper about it, and a few days later there was already a 250k line lean program claiming to verify it.
It’s highly nontrivial to verify that a 250k loc Lean program actually represents that which it claims. I guess it could be AI turtles checking and summarizing all the way down, but is that any more credible than a single AI checking it? I doubt it.
No country for mediocre mathematicians
41–50 of 159 posts
Re: No country for mediocre mathematicians
#42Hard disagree.
Lying is with intention to deceive.
Teaching is simplifying with the intention that they understand and get the correct intuition.
Math is not about lying, that's just silly.
Re: No country for mediocre mathematicians
#43Earlier quoted context omitted.
Yeah seems like most programmers just do it for the money. I imagine only like 20% of us do it just because we enjoy it.
True. I like math and CS theory, but despise coding (pays well though). AI is finally taking over this soul-sucking occupation and all I can say - good riddance.
Tbf coding with ai is still super fun though. I am hoping that engs who hate it like you will finally get kicked out as productivity increases from ai and it will finally go back to just us nerds.
It's kinda soul-sucking being around all you guys that just hate this work, please get out and go do farming or something lol.
Re: No country for mediocre mathematicians
#44> Lying is a core part of communicating mathematics. We lie to kindergarteners when explaining fractions. We lie to fourth graders when approaching limits... Hard disagree. Lying is with intention to deceive. Teaching is simplifying with the intention that they understand and get the correct intuition. Math is not about lying, that's just silly.
> As humans, we have invented lots of useful kinds of lie. As well as lies-to-children ('as much as they can understand') there are lies-to-bosses ('as much as they need to know') lies-to-patients ('they won't worry about what they don't know') and, for all sorts of reasons, lies-to-ourselves.
> Lies-to-children is simply a prevalent and necessary kind of lie. Universities are very familiar with bright, qualified school-leavers who arrive and then go into shock on finding that biology or physics isn't quite what they've been taught so far. 'Yes, but you needed to understand that,' they are told, 'so that now we can tell you why it isn't exactly true.'
> Discworld teachers know this, and use it to demonstrate why universities are truly storehouses of knowledge: students arrive from school confident that they know very nearly everything, and they leave years later certain that they know practically nothing. Where did the knowledge go in the meantime? Into the university, of course, where it is carefully dried and stored.
Re: No country for mediocre mathematicians
#45I have some bad news for the non-mediocre mathematics. Given it another year or two or so and there won't be much need for non-mediocre mathematics either. Instead everyone will have on call a near magic mathematician who can push the state of the art for their needs. Math is actually a perfect fit for AI because it is possible to express everything in terms of written language and you can write formal verifications…
Re: No country for mediocre mathematicians
#46Earlier quoted context omitted.
I’m not sure about this. Anthropic’s AI constructed complex structures on S^6 and wrote a 108 page paper about it, and a few days later there was already a 250k line lean program claiming to verify it.
It’s highly nontrivial to verify that a 250k loc Lean program actually represents that which it claims. I guess it could be AI turtles checking and summarizing all the way down, but is that any more credible than a single AI checking it? I doubt it.
Generally you only need to look at 10-100 lines (unless you have a highly novel theorem that essentially invents a new field of math or builds on a field that has never been worked on in Lean before) of the 250k to verify what it claims. This is why there is excitement around formal verification. The rest of it is perhaps useful to read to figure out why the proof works, but is not necessary for checking.
Re: No country for mediocre mathematicians
#47> My physicist friend once asked me what the point of doing research was if someone like Terence Tao could have figured out everything in my dissertation in a tenth of the time. I answered by pointing out that Terence Tao didn’t. Terence Tao did not find a small open problem posited by my advisor and publish a bite sized result making incremental progress. He has only so much time and so many other fish to fry. This…
> what the point of doing research was if someone like Terence Tao could have figured out everything A similar question is now being asked: what is the point of doing research, etc. if something like AI can figure out everything? The question betrays the parochial way in which many people think about knowledge. For them, knowledge is merely an instrument or an effect. It does not occur to them that knowing is a valua…
A brief example: When I was a teenager I had the most profound crush on a girl, as teenagers do. Gorgeous and gregarious, she was often surrounded by a circle of friends and acquaintances, and I noticed the peculiar way in which she would give attention to each in turn. She would exchange a few sentences with them, and then maybe her head would turn a certain way or her eyes would glance elsewhere, and that's how you knew your time was up and she had moved on to the next. To continue the conversation you had to hold onto the state in your head and wait for the next go around.
From her I learned a lot about how multitasking works, and how task schedulers distribute little quanta of time for each task to do some work before moving onto the next, and how this was achieved in cooperative multitasking by mutual communication between the task and the scheduler.
Would a vibe coder be able to have that insight? Maybe, but would they have been able to elaborate it into a working implementation? Perhaps, but I suspect with more time and difficulty than I did, because both the initial insight and the elaboration of detail that let me show that it worked lived in my head, not in some ephemeral AI context.
Re: No country for mediocre mathematicians
#48Re: No country for mediocre mathematicians
#49 For every landmark theory, theorem, or conjecture, there have been incremental, partial results supporting intuition and inching towards the white whale. When I attended BARD, a small computational number theory conference, one of the organizers preached of the outsized impact we could have just by being willing to program the numerical experiments that other mathematicians only theorized about. The small ball player can completely change the approach and intuition of the leading names without ever joining their ranks. The mediocre mathematician has always had purpose.
Yes, yes, YES! F*cking yes.The greatest challenge of the AI Age (which is also the Climate Change Age and the Demographic Trap Age and a lot of other ages) is going to be finding an appreciation of the mediocre and mundane, when so many things are going very right, and so many things are going very wrong. Most of the time, the top of the bell and an SD in either direction can overwhelm either end, for better or worse. So respect for the unremarkable is warranted, if you want good things to happen and bad things not to.
Re: No country for mediocre mathematicians
#50Earlier quoted context omitted.
Whenever there is a breaking AI-generated proof, it's the job of actual leading mathematicians to formalize/check it . Laypeople are not checking or writing these AI-assisted proofs. Even when Lean is used, it's mathematicians writing these proofs and checking if the formalization was done right. Terrance Tao's career trajectory has reached new highs due to AI. He's more relevant than ever. This is the exact opposite…
honestly curious question: do you expect this to remain true? If so, for how long? I can think of two potential reasons why it might not stay true. 1. The very best humans remain able to understand/check the proofs, but we go for so long with every proof checking out that society more broadly just decides to trust. We are already doing that with human mathematicians. I can't verify what Terence Tao tells me is correc…
It's already the case that it's becoming not true. For example see this post from Lin Yang: https://x.com/lyang36/status/2092092709251293611
"Throughout the process, I felt that my only role was to teach the AI how to write things in a way that I could understand. Its initial language was extremely condensed—so compressed that I could barely follow it—but somehow the AI agents themselves seemed to understand it perfectly well."
It won't take much longer before AI is consistently better at validation than humans, and at that point, why continue to have humans do the validation? I think we're being naive about the end game - admittedly I don't know what it is though.