As someone who mostly only applies math, that strikes me as a peculiarly academic take. Intuition is more important for me because it’s what enables me to know what methods are most applicable to whatever practical problem I’m trying to solve. The proof’s purpose is to verify my intuition. It’s just a means to an end. I only take the time to do my own when I can’t confirm what I need from a textbook or paper.

>You cannot do proof without intuition hence, if you emphasize proof, intuition will take care of itself.

This isn't always the case. Our algebra (or analysis) course focused a lot on proofs for the exam. The result was that a lot of people learned the proofs by heart.

Surely this implies these LLM generated proofs require the LLMs to have mathematical intuition . . . and honestly I don't think many people believe that, and rightly so, certainly not in the way Poincaré was on about.

Maybe it's been done, but I'd like to see an LLM recreate Euclid from questioning without having seen it during training.

As a math professor, I care much more about the key idea, heuristics, and motivation than the proof. With the others in place the proof is clear, something an AI or a student can do.

To agree:

In my experience, proof is the gym reps that allows you to harness strong intuition elsewhere.

In practice as an engineer, intuition is far more useful, eg, being able to “feel” when something is off in our reasoning — but proofs are where I train those same sensibilities on “harder” problems, (eg) details about how to model identity, equality, and equivalence in a formal model.

> Open source programs could be more like motivated explanations of computation.

It is already that. Every time a method/function is created, a structure is defined, a variable is added, a file is created or renamed,… It’s all for the purpose of human communication. The computer only need binary in a single file.

But people feels like they should be able to jumpninto curl code without any understanding of networking, or linux code with no knowlede of computer architecture. Few code are meant for total beginners.

Programming was never about communication. It was always about making the machine do the thing we want. Back in the day, a good game programmer knew which time intervals had writable video memory and which CPU cycles drew which scanlines, and spent more time rearranging the code to hit these timings than to write the actual algorithm. Later programmers (I hesitate to call them good) learned everything there is to learn about OS internals and wrote theoretically nonsensical and invalid code that still worked thanks to those internals, to save CPU cycles and especially memory use. And the next generation of programmers took the principles of late binding and abstraction to the logical extreme and created architectures that cannot be described in words anymore, only in diagrams - but are crazy good for code reuse, traceability and A/B testing.

This feels a bit too optimistic regarding programming. Or perhaps betrays an imprecise definition of programming. To me, programming is about expressing algorithms. But algorithms may be totally illegible and still work fine.

Math on the other hand is exclusively about being understood. It is ideas from math that made algorithms legible and thus made the act of programming an act of communication. If by programming you mean using notation and ideas that were borrowed from mathematics to specify algorithms, then for sure it’s communication, but only inasmuch as it was math first. If you mean only specifying algorithms, then no communication need take place; the executor of the algorithm will deterministically execute it irrespective of its ability to communicate.

> usually by people who are good mathematicians but know close to nothing about teaching.

I higly doubt that. Maybe in university level courses. Most people’s only experience with mathematics is an elementary or high school teacher who were probably themselves at best mediocre at the subject. Simply because of selection factors. Those who are good at math are encouraged to go into STEM. There will be of course exceptions everywhere, but that is not what “usually” happens.

And thats just about being good at maths the school subject, which is distinct from being “ good mathematicians” the science / research topic. Mathematicians are few and far between, simply because it is a specialist subject. There just aren’t enough of them to go around for them to be the formative experience around math for most people.

Another response to math that makes me sad: "I must be too stupid to understand this," "my brain is too small for this," etc. Different people say it for different reasons, but it's almost always in response to a hand-wavey explanation that doesn't makes sense to anyone not already in the know. Math is so much more about humility and skepticism than it is prodigy.

> People often hate math because it was not explained to them correctly

Spoiler: this is also why mathematicians hate vibe-math. AIs are outright terrible explainers even when they do have a watertight logical argument—and honestly, this is the load-bearing seam.

It goes beyond "proof vs. exposition": the logical derivations AI comes up with fail to even qualify as human-directed proof because of how terrible they are (far below even the most novice mathematician doing their roughest work) at the exposition part.

a good teacher remembers the journey, not just the destination.

socratic method exists. almost none follows it.

'From which it is obvious that...'

I actually have a rather dim view of the "writing code was never the point" line. Not because it's objectively wrong, but because I see it as something we're mostly telling ourselves to feel better about the status quo. Ability to write good code has been highly celebrated (and remunerated) for decades. As it is becoming less relevant, we immediately backtrack and start lionizing the parts where we can still be useful instead. Consider the counterfactual - AI continued to be terrible at writing code, but weirdly better at humans at product decisions, architecture etc. In this universe, saying "coding was never the point" would not be popular.

It also find little solace in it aside from 'well this version of GPT isn't taking your job'. AI labs certainly have no intention for the higher level skills to stay in the human-only domain. The veteran developer with the coherent theory of a large stack is immensely valuable today. But they also don't survive if a company can drop a few coders' salaries on rewriting that stack from scratch - faster, fewer bugs, more coherent, able to react to changing business requirements with more agility etc. I am not saying this is where we are, but I think there is a reasonably good chance this is where our road is leading us.

Isn't it kind of inevitable? As long as humans have the desire for power and control, informational networks will be developed and extended until the point of replacement of humanity because it will be in some parts interest to use them to accumulate power.

You're asking to go against evolutionary principles to reject the utopia. Everyone on earth will never agree to become monks, there will always be the desire to reproduce better, signal status and power, so the technology will be developed until we are finished as a species.

I've already seen this sentiment expressed in the wild.

Im an ex mathematitian too. And if i was in academia I would probably have the same reaction. Thats what i say that its the worst time for proving economic value.

But if you are in for theory building and understanding, then you are not constrained anymore by your motivation to grind through countless hours of formal theorem proving. And you do not need to have superhuman formal manipulation skills and memory.

For me mathematics is not the formal system, so LLMs will never be able to do end to end maths.

But these are not very good arguments, because it makes it about the fall of institutions (the funding) and people being miserable for personal reasons rather than prosocial reasons. Tao here clearly suggests that math is not reducible to "problem solving" or "proofs", the valuable part is much more than that framing.

The concerning argument about the status of math would be an outline that it will get destroyed by a process of societal atrophy and there is no turning back, and the AI powers are not a good substitute or replacement for it. If an entire society becomes reliant on these oracle machines then it would be analogous to children never learning arithmetic because they were handed calculators. How could the human race still flourish? We would anthropologically regress. We'd be little better than animals, like the Borg zombies.

That is a much more profound threat than people worrying about their own careers or faculties disappearing like the humanities. This is a serious anthropological reckoning.

If math experts are that freaked out already then basically all of science is soon to follow, decade by decade. "Singularity" comes to mind.

> As an ex-mathematician I assure you this is very wrong, and every working mathematician I know right now is completely miserable, and/or trying to flee the field as fast as possible.

To throw a counterpoint to this into the writhing cesspit of HN, I'm active in academic mathematics (postdoc) and every one of my collaborators is deeply in love with the field and their jobs. Perhaps the grass is greener on the applied mathematics side of the fence.

Probably true for the dedicated problem solvers (of which Tao is one IMO). But I doubt there's ever been a better time to be a theory builder (more like Peter Scholze, or Grothendieck).

Some up with an idea and leave the system to check it 15 different ways, and see whether you can simplify an existing body of theory. It'd be like having an army of lightning-fast grad students.

That's not the conclusion. I started using AI after the Jacobian conjecture counterexample and have used a particular problem to learn how to use AI and to explore it's capabilities. I'm not a great mathematician but I'm full faculty with 25+ years of research experience and lots of articles and I just proved in a few weeks something that had resisted my efforts for some years.

The exploration process is much easier now. Ideas are quickly testable and multiple tests can help identify a technical obstruction. The tool requires good guidance and input but as it trains on people like me it will need those less.

At the very least our way of doing things must change. More pessimistic views seem to me defensible.