you cannot be mathematically rigorous with computational lower bounds. It is not possible with current mathematics. No ones that are relevant to cryptography exist, so any computational cryptography must separate into

1. provable constructions based on "hard" problems, and 2. best-effort cryptanalysis of "hard" problems.

This is true of lattice-based problems. It is true of EC crypto. It is true of RSA. it is true of McCliece. It is true of AES. That is the nature of things, and there is no avoiding that.

Analysis of Kyber was honest and mathematically rigorous. It's also beside the point, as all of your criticisms hold for EC/AES as well (despite EC having some reasonable lower bounds, e.g. in (extensions of the) generic group model. These of course rely on the conjecture that EC groups are generic groups).

> We should be working on standardising and moving towards methods that are independent of, rather than rely on, unresolved questions in mathematics.

There are no known methods that are remotely economically viable. There is (completely seriously) a clearer path towards fixing climate change than what you say. There is also a clearer path towards fixing global hunger. It is a complete fantasy to want to solely rely on mathematically provable techniques in cryptography, and not one that it is worth engaging with.

Furthermore, it's completely pointless. We might as well frame your question as

> We cannot prove that AES is hard, so we should not use it.

Why? It would be cool to prove that AES is hard. Sounds fun. And practically, the hardness assumptions of deployed cryptography are almost never the cause of a security vulnerability. If we care about secure systems, proving AES is hard is so low down on the priority list that it is difficult to think of something less important. Again, completely seriously, we would have MUCH more secure systems if we paid each person in the country to use better passwords.

Given that this is the case, it seems unreasonable to suggest spending \Omega(billions) updating our network infrastructure to worse-performing links just to "fix" a problem that doesn't exist. I'm even speaking as a cryptographer who (unreasonably) dislikes heuristics in the field, and tries to replace them with provable alternatives. It is a fun academic exercise. But it is not a real world issue.