I agree, but... Spend time formalising a large part of existing mathematics and proofs, train a bunch of sufficiently powerful and generative models with that, and with cooperative problem solving and proof strategies, and give them access to proof assistants and adequate compute resources, and something interesting could happen.

I suspect the barrier is finding a business model that would pay for this. Turning mathematics into an industrial, extruded-on-demand product might work, but I dont know who (except maybe the NSA) would stump-up the money.

Could you expand on this? I don't see maths as a language for quantities specifically (i.e. what does symmetry have to do with quantities).

> just too tedious (but not impossible) for a human being to work through the proof.

Already happened with the four colour theorem arguably.

That’s easily proven to be true. “Two plus two equals four” is a theorem, so is “three plus three equals six”, etc.

This is a somewhat bleak picture of math. We also have the other phenomena of increasing simplicity. Both statements and proofs becoming more straightforward and simple after one has access to deeper mathematical constructions.

For example : Bezout's theorem would like to state that two curves of degree m, degree n would intersect in mn points. Except that you have two parallel lines intersecting at 0 instead of 1.1 =1 point, two disjoint circles intersect at 0 instead of 2.2=4 points, a line tangent to a circle intersecting at 1 point instead of 1.2=2 points. These exceptions merge into a simple picture once one goes to projective space, complex numbers and schemes. Complex numbers lead to lots of other instances of simplicity.

Similarly, proofs can become simple where before one had complicated ad-hoc reasoning.

Feynman once made the same point of laws of physics where in contrast to someone figuring out rules of chess by looking at games where they first figure out basic rules(how pieces move) and then moves to complex exceptions(en passant, pawn promotion), what often happens in physics is that different sets of rules for apparently distinct phenomena become aspects of a unity (ex: heat, light, sound were seen as distinct things but now are all seen as movements of particles; unification of electricity and magnetism).

Of course, this unification pursuit is never complete. Mathematics books/papers constantly seem to pull a rabbit out of a hat. This leads to 'motivation' questions for why such a construction/expression/definition was made. For a few of those questions, the answer only becomes clear after more research.

= I live in California, and the nearest Starbucks is more than 20 miles away.

>>can only be contacted during a full moon

= As a night person, I am awake when the streetlight outside my house turns on.

>>certain arcane rites that are too horrible to speak of

= In order to contact me, you must install Microsoft Teams.

Overall, it's not that bad, except for the MS team thing. ;)

https://en.wikipedia.org/wiki/Alexander_Grothendieck#Retirem...

"Local villagers helped sustain him with a more varied diet after he tried to live on a staple of dandelion soup." - like most people would.

But it did. Painter used to be a trade where you could sell your painting skills as, well, a skill applicable for other than purely aesthetic reasons, simply because there were no other ways to document the world around you. It just isn't anymore because of cameras. Professional oil portrait painter isn't a career in 2025.