YHK - yet another hacker news clone

> It will grow into a full-scale industry and become the true infrastructure of all scientific and technological progress, a foundation that every other field stands on rather than a quiet corner of academia.

Sounds revolting. Everything being turned into the industry is soulless and uninspiring. I know a lot of people worship this future but I for one hate it. I for one don't see the point in creating this intellectual power where there will always, always be someone to abuse it simply because of our instinct to be greedy.

The notion that mathematics would be over just because it's slightly easier to find proofs is like the idea that astronomy would be over because of telescopes.

This is probably the inescapable conclusion that most in the current panic-filled era of Math research discourse will come to, one way or another.

Not sure why people are stopping at 'AI can do advanced math!' and calling that the field is gonna transform due to LLMs specifically. Pretty much any meta-formulation of math gives you some initial rules and a goal. From natural deduction and sequent calculus to dependent type theory and whatever flavour of category theory you choose, at a sufficiently abstract level, you'll end up with some form of search problem. ATP folks foresaw machines doing automatic proofing for decades, but it seems that noone had enough incentive in pursuing it at the cost of suffering the tediousness of the encoding process. Now AI labs took the opportunity to do something impressive and have shown that it's possible to close the ergonomics gap. But the deeper achievement is the decades of ATP and proof-assistant work that make machine-generated proofs mechanically certifiable in the first place.

I am pretty sure in the next couple of years we'll see more evolved sledgehammers [0], maybe with LLM-like tech playing a role in encoding theorems, that will allow us to prove deeper than we can do manually, then help with the archeology and extraction of learnings from observing the 'trace' of certified proofs. So instead of explore -> understand -> solve, we'll get solve -> compress -> understand.

[0] e.g. https://isabelle.in.tum.de/website-Isabelle2025/dist/Isabell...

This piece reminded me, of all things, of Gandhi's essay "Hind Swaraj." He was pretty anti-technological-driven change.

He was anti: - Machinery replacing handicraft (skill disappeared and poverty followed) - Labor-saving machines replacing human workers (workers became expendable) - Doctors replacing consequences (people lost self-control) - Railways replacing constraint and slowness (harm spread faster)

But he loved the sewing machine.

Gandhi’s test for whether to accept tech-driven change was whether it satisfied primary needs. Interpretation of those needs was certainly not universal. As he wrote: "...it is not the primary need of man to traverse distances with the rapidity of a motor car. The needle on the contrary happens to be an essential thing in life, a primary need.”

That's the airplane in this post. Excitement or fear of the AI airplane is either judged as helping mathematicians (sewing machine) or doing something not quite right (the above machinery/doctor/railway)...