Math is more about figuring out why things are true than what is true.
Mathematicians want to understand Mochizuki. They couldn't care less if hn thinks it counts.
Mathematicians want to understand Mochizuki. They couldn't care less if hn thinks it counts.
At the point that we no longer understand the relationship between the formal proof witnesses (and really, the class of possible witnesses) and the axioms we choose, we can no longer do mathematics, because we can no longer meaningfully explore axioms -- our ability to make guided changes is destroyed by our inability to understand their effect.
It's important for the community to understand something of why a thing, not just that it's true, because that's why drives the development of mathematics forward. (And indeed, particularly so in the ABC conjecture, which sits at a node between the nature of multiplication and addition, which don't usually have much to do with each other.)
I actually wonder if US (and perhaps other) math education is harmful here: the focus on rote learning and just knowing that a thing is true (to mechanistically apply it) has conditioned people to not understand why the hesitance over proofs that humans don't understand -- for most of those people, they never understood the proofs anyway.
Sometimes I'm saddened that this future may come slower than we'd like due to imperfect funding structures. But I've grown a lot of patience over the years :)
I was just pointing out that the person got flagged for commenting that "witness and dump" isn't actually very useful for mathematics as a field, except as a signal that we should investigate a topic further. But in the case of the ABC conjecture, we already have plenty of incentive to investigate.
I think mathematics and science have a lot of learn from computer science in terms of managing large models, proofs, etc -- and that we'll get a lot of automatic tools. That will all be really great.
But there are proofs that are basically just brute-forcing a solution for which we have no higher-level understanding, and those don't really add much by way of knowledge to mathematics. At the point that those are all we can generate for "big" problems, we may be in trouble.
That a function is the same thing as a proof, with the theorem it proves being the type it constructs and its assumptions being the types it takes in. (Functions are proofs (which in this case, are things that take witnesses of their assumptions and produce witnesses of their theorem), values are witnesses that something is true, types are theorems, etc.)
I have an interest in topology, and want to understand HoTT, but my intuition around type theory wasn't up to par -- so I'm trying to tackle it in a constrained setting (ie, not proving theorems about mathematics as such, but a narrower problem space). Figured there was nothing to do besides get into the messy bits of it.
Can you tell me a bit more about what you're trying to do?
Do you have any suggestions for simple introductions to HoTT, especially for someone without the topology background?
It's then using that equivalence structure between the proofs to reason about constructing proofs, as you can reason about the constructions that are possible out of classes of proofs. And that's basically where I get lost, because I don't quite know enough type theory to understand the structure they're trying to build, so I can't quite get the specific motivations. (The obvious high-level one is better formal reasoning.)
I haven't been following HoTT super closely for a year or two, getting sidetracked into the background, but last I checked there wasn't a ton of simple material on it -- it was sort of read the book, read the Coq proofs/framework, and figure it out. (Though, this easily could have changed.)
That almost sounds like "the future is mechanically composed novels" (or music). Understanding why something is true is just as important as knowing that it is. Mechanical proofs will be impossible for humans to understand, so the value of such proofs will be rather limited (in that people will still continue searching for a "real" proof).
For some value of "future" - sure, maybe. But the vast majority of theorem solutions do not lend themselves to mechanical proofing, and it takes great effort to do it at all.
I don't really agree with your thesis here. I don't see how we're going to get to a future where we're tackling much harder proofs, because the hardness is already what prevents them from being so easily mechanized and checked in an automated manner. We have no problem coming up with new theorems, either - half the job of a pure math researcher is coming up with interesting questions that are too hard to solve immediately but not quite so hard that they're inaccessible.
The only way to make the proofs "harder" is to make theorems that are even further removed from our current mathematical capabilities. Otherwise you're stepping into the undecidable territory. Simply put - solving open problems is a major activity in mathematics because it develops new mathematics, not because the actual end result is useful in of itself. If I prove to you that Pi is normal, the fundamental contribution is (hopefully) a method that is partially or fully generalizable to other domains. No one really cares if Pi itself is normal, and most already expect it to be. To mechanize that process (if it's even possible at all) requires that the mathematics for solving it already exists, which means that the problem is most likely either 1) uninteresting, 2) overlooked.
Hopefully that can propagate upward.