Hmmh. I like motivated explanations, but, as acknowledged in the text, this is a subjective thing to measure. What is a great motivated explanation for Tao, might be hard to grasp for me. So I guess judging how well an explanation motivates something depends on two things: 1) My way of thinking, and 2) what I already know and how well I recall it in this context.
There is a third thing: how well does the motivation chime with or go against my current belief system? You would think this is not much of an issue in mathematics, but it can be, and I had my fair share of frustrations because of it.
Anyway, all of the above points to one thing: the best motivated explanation will be generated by an AI, knowing the subject and you in a deep way that no other human will, and being able to interact with you during the explanation.
> 1) My way of thinking, and 2) what I already know and how well I recall it in this context.
I don't think we're discussing pedagogy. Good _research_ exposition is instead related to communicate your intuition and way of seeing things. The conceptualization of a given situation or problem is what is valuable, how you connect it with other stuff, etc. It is then up to you to memorize and interiorize it.
Seems to me to be two different sides of the same coin. Pedagogy is about finding a way to communicate to me an idea based on my intuition and seeing things. A research exposition is about presenting the idea in terms of your intuition and seeing things.
Good research exposition is the same as good "pedagogy" just for a different audience. Both have to consider didactics. When writing a paper, you teach something to the fellow researchers who know less about a thing than you.
The blog post says that the statement "AI really did solve a problem in mathematics." is wrong. But a formal proof showing that Navier-Stokes equations can blow up is certainly such a solution, by AI. There is not much in this world that is more objective than a formal proof, so any disagreement on this is based on how we see the world. Michael Harris will agree with the statement being wrong, Jacob Tsimerman will not.
Another example, Hilbert famously battled Brouwer's view of mathematics. From my point of view, Hilbert was right: intuitionistic logic is certainly interesting; but I like to study it using "normal" (= classical) mathematics.
Finally, my personal frustrations are about how hard it is to publish my work on abstraction logic. I would never have thought it is that difficult, mathematics being objective and all. It seems essential to take out as much motivation out of your paper as possible, because it might offend your reviewers and their belief system. By now my papers come with full Isabelle/HOL formalisations, let's see if that helps.
Isabelle is actually a "logical framework", so it supports intuitionistic logic, actually its meta theory is intuitionistic higher-order logic.
So this is not because of the logic, it is because of the mindset. Intuitionistic logic is usually championed by people who want to emphasise computation over reasoning, and that is why they build computation as one their reasoning steps into their kernel. They don't have to do that. They do it deliberately, because it aligns with what they like, and how they like to think about logic.
In HOL Light? Just so you can run the proof objects through another prover like Isabelle. Wasn't that your original ambition?
As you know, Rocq and Lean folk want more than just that from their proof objects. They want proofs to contain executable code, often of the very programs they were verifying, and so treat their proof assistants like programming languages with verifiers attached. So you get complex recursion and inductive definitions baked into the kernel. Whether this is a good idea or not is obviously pretty disputed among us, though I'm mostly with you and Larry :)
> So you get complex recursion and inductive definitions baked into the kernel.
It is a pragmatic choice, just like a type system is. I think both of these choices are outdated now that formalisation is fast. What you really want is a simple semantics (what is the semantics of Lean again...?), and build on top of that by verified kernel extensions. Program extraction via proof objects doesn't really work, I don't think anyone does that for real. What you do is you write your program in your term language, and export the meaning of that term as a program. Isabelle does that, too, and you don't need proof objects for that.
In my current version of Practal (Practal Zero) I have a switch for keeping proof objects around as well, in case I want to maybe transform proofs in some reuse scenario. Not sure if I will actually use that, ever, because it would be slow, too. Also, I would rather prove that a certain transformation is correct, and then add this as a kernel extension.
That's right, they become part of the replay and rejected using the same path, otherwise things like cycles might still happen. Rejected ops do stay part of the log though, so there's always ways to build time travel/version history or conflict UIs on top when needed.
One of my favourite books of all time is by her: The Dispossessed.
It "features the development of the mathematical theory underlying a fictional ansible, a device capable of faster-than-light communication, which can send messages without delay, even between star systems." [1]
It doesn't get better than that. Certainly not "harder".
I actually think it is just the dawn of mathematics. During the last few days I discussed a few questions about abstraction logic [1] with AI that I was wondering about for quite some time (years), but didn't have the time + energy + in-depth expertise, there were like, 4 related questions; it positively solved 3 for me in the way I expected, but couldn't power through before; and for the fourth it proved to me that answering this question would imply solving a known open problem. And I know that it answered all of those questions correctly because I asked it to provide me with Isabelle/HOL proofs for it.
If you are interested in mathematics because it can model things precisely, and you want precise answers about these models, and you want to know how it is all connected (Langlands anyone?), AI is fantastic news. There is plenty of new and interesting and beautiful and elegant mathematics to be had this way, as well.
This is not a time to be scared or frightened. This is a time to be excited as fuck.
There will always be open questions. Now, there will be actually many more of them, because many more people will be asking questions.
There is a third thing: how well does the motivation chime with or go against my current belief system? You would think this is not much of an issue in mathematics, but it can be, and I had my fair share of frustrations because of it.
Anyway, all of the above points to one thing: the best motivated explanation will be generated by an AI, knowing the subject and you in a deep way that no other human will, and being able to interact with you during the explanation.