> It's like they can't step back from the problem and realise that they need to simplify to make it work better. Nope, just keep hammering more code/proofs against the problem and eventually you'll hit the goal.

There is nothing wrong with that approach if it accomplishes the goal faster, i.e. you can work at the speed of an AI.

> There is nothing wrong with that approach if it accomplishes the goal faster, i.e. you can work at the speed of an AI.

Sure, and god knows I've done the same myself when under time pressure (so similar to an AI in RL training, just get the goal).

The part that's lacking (that humans are much better at right now) is the meta-cognition around this works, but it's far more complicated than it needs to be.

Potentially because LLMs have larger "working memory" than humans, they can avoid this for a while, but once it blows up the context they fail in much worse ways than a human would.

Hmmm, this feels like a good metaphor, I need to write about this at some point.

Funny enough.

There is ongoing AI assisted work on this, and precisely the problematic gap in the theory (around Corollary 3.12).

As of now, a required step appears to definitely be missing, but it's not clear if this is a genuine / unrepairable defect.

https://zen.ac.jp/news/zmcpostevent0331e

https://github.com/lana-agents/iut

https://github.com/LANA-Project/genl

>I think it's not just to check - it's to interpret, simplify, apply taste, basically get these proofs into a form that humans can grok and build on.

Sure, but we are approaching a time at which we will have to answer a "why" here. I.e. anything beyond checking and validation becomes of mostly artistic value at some point. And there is nothing wrong with that.

IMHO it's groking that allows higher level metaphors and eventually more powerful theories to be built. If all you are doing is proving everything reachable by construction, you aren't really learning, as this process won't be drawn to the more compressed expressions by necessity but only as a "please" from the humans.

I’d say the artistic value is the main value in general —- if you know mathematicians they will often refer to a ‘beautiful’ proof, aesthetics is a critical part of math.

An early (easy to understand) proof that fits the bill for me is proof that the sqrt(2) is irrational: a very natural thing to think about —- for a unit square, what is the measure of the diagonal? And people were killed in ancient Greece over the proof, but it’s comprehensible with basic algebra.

I think you are slightly missing the mark of the historical reference.

What you say is true for modernized budō disciplines. They have very different purposes.

But this this is not what Musashi was concerned with. He was practicing kenjutsu (not kendo) / writing about hyōhō.

The primary criterion was absolutely murdering people as efficiently as possible in a life and death situation.

"The true Way of sword fencing is the craft of defeating the enemy in a fight, and nothing other than this"