Comment by sigbottle

Will we ever run into a theory of meaning crisis?

_Assuming_ two failure modes:

- The lean kernel could always have a bug. - The formalized statement may not correspond to what _mathematicians_ "actually wanted"

It seems natural to make the argument of, "Well, even if you make the argument that the proof can have mistakes, it's surely easier to check the problem statement of something rather than the solution".

(A "nice property" is that, the agent doesn't need to even get "subarguments correct" according to the _second_ criteria - maybe in the natural proof it invents an object subtly different from the formal one, but it all checks out. If you guarantee that the _original_ statement corresponds, then the only possibility is the lean kernel. So it doesn't recurse infinitely, in this case).

But "definitions" are always a really weird thing that I don't think we have good theories for? How do you quantify how much descriptive power you need to express a question? Often times in math, the hard part is getting the definition right - but what if the definition itself starts to become so complex and unverifiable that no one can correspond that to anything? Well, it seems like many interesting long-standing math problems have "relatively" simple problem statements, in such a way that you could formalize it to lean easily, but not sure if there's really a silver bullet w/ lean or if it's going to be turtles all the way down.

It probably doesn't matter as long as AI keeps skyrocketing on the much more general property that is "intelligence", but still. Interesting to think about.

(Well, this is where AIT gets actually interesting, but still, I don't think its a generalized theory of semantics.)