practal

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.

One example is what currently plays out, see the previous guest post on Tao's page: https://terrytao.wordpress.com/2026/09/12/after-math/

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.

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.

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.

> 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.

I added proof objects ages ago to HOL Light, it is not a big deal. It's just, as Larry said, why would you want them in the first place?

So what happens with optimistic local operations that become invalid after replay of canonical operations? Are they just thrown away as well?

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".

[1] https://en.wikipedia.org/wiki/The_Dispossessed

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.

[1] http://abstractionlogic.com

I think 6) is a very good point. The simple reaction to it is, well, I just define a small verification kernel that I trust, and the rest is just scaffolding that does not need to be trusted in order to have full confidence in the verification. Of course, that is not really true, because how do you know that the data arrives properly at the kernel, and is properly read off the kernel? In practice though, the small verification kernel idea works very well. I don't think that this is the final stage of how these systems are designed, though. I think we need to model the full system inside the system, and verify it this way. We can trust this verification because we are verifying it with a system with a small verification kernel, but afterwards, we can replace the small kernel with the modules we have proven to be correct now.

TU Munich and Nipkow, Makarius et.al. are also at the center of the influential Isabelle theorem prover. TU Munich is cool :-)

I agree with that, that's why I am starting with plain syntax first in https://zero.practal.com, because that is really where all the information/logic lives. But there will also be a presentation layer on top of that, building on the information layer, so with time, I would expect it also to subsume much latex/typst functionality. The "header semantics" I already copied from Markdown.

How did you get suspended for 8 hours, given a 5-hour window? Maybe you are prompting it wrong [1].

[1] https://www.wired.com/2010/06/iphone-4-holding-it-wrong/

I used it yesterday afternoon-night and this morning-afternoon, UK time, over a period of a few 5-hour windows. I didn't count the prompts, wall time was 1d6h, API time was 2h10m.

I am quite impressed with Fable 5. I used the £18 subscription, and asked it to convert the document processing of Practal Zero [1] from running in the same thread as the UI to a worker thread. Just two days before I gave the same task to Codex, and the result was not really nice: it would copy the entire document to the worker thread as a snapshot for processing, and so on. Fable instead realised that it could make use of the fact that I have a self-made custom database based on operational transform running (that's why document loading is so slow :-)), and made the document processing to be just another client of that database. It discovered even a bug in how I sync between the "livemodel" (in-memory replica of database state) and ProseMirror's model. That sync made problems before, and I had written a spec up for that, convinced that my "fourth attempt" at it would be correct. Fable found a last bug in the spec, corrected it via a "fifth attempt", and fixed the corresponding code.

The reported API costs for all of that would have been $180 though, which I cannot afford when the Fable promo ends on June 22nd. I am also a happy user of £89 Codex, it is really reliable and works very well, but Fable seems to be just noticeably smarter.

[1] https://zero.practal.com

To add, what also often happens in these discussions is that Codex suggests a design that makes no real sense at all, or that it brings up two or three design alternatives, and recommends exactly the wrong one.

On Saturday I thought I had vibe coded myself into a mess. I had implemented a new block type in my structured editor for Practal Zero (or rather let Codex do it), and suddenly the syntax highlighting broke in the whole document. Asking Codex to fix it didn't work. I was contemplating to restart the whole project on a basis that I actually fully understand, but that would set me back so much when the first reasonable prototype seemed so close. Instead, I took a walk.

See, the project actually has a well thought out structure that I design carefully, but more and more of it gets filled out by Codex. Codex is not smart enough to remember all the high-level design considerations, some of which had not been documented because I was just implicitly assuming them. So the fix was to use Codex to isolate the error, think about in terms of the high-level design, and fix the problem, which was partially an implementation problem, and partially a problem of the high-level design.

I fixed the high-level design with discussions with Codex, and documenting this, and then let Codex implement the fixes. The discussion took me more than an hour, the implementation was done in a few minutes.

This working style is similar to doing math: You have a high-level idea of what you are doing, and let that guide you, and Codex assumes the role of something that fills out all of the details you take for granted. Often it turns out your high-level idea had flaws, and this shows up in your code not working as expected. So you revise your high-level idea, refactor the code to reflect the modified high-level design, rinse and repeat.

Working this way is still really hard, but it allows me to do things I could not have done before. Getting your ideas validated (or refuted) in minutes instead of days is huge, and makes it possible to march through stuff that would have turned into a deadly swamp before, at least for me.

Now. Do I think that most corporate programmers will use Codex or CC in this way? I don't know, but I think probably not. So what will stop them going into the swamp until it swallows them, instead of backing up in time and marching around it?

Super. I always wanted to learn about sheaves and schemes and the like, and this gives a simple introduction that really motivates digging deeper into the details.

It is also immediately clear why this plays a role in semantics for logics: although a ring is not that important in logic (I would think), the idea to study a theory through its syntactical consequences turned into semantics is very natural, and exactly what I do for abstraction logic as well, in particular via "valuation spaces". And it has the same property, once you set up everything the right way, things like completeness just automatically flow out of it.

> Even more important than lemmas are observations, but that is another story.

In my book about abstraction logic (http://abstractionlogic.com) I have definitions, theorems, lemmas, and even observations :-) Just did a count of the frequency. Of course, not sure what those frequencies say about the relative importance.

-----------

Definitions 78

Theorems 20

Lemmas 76

Observations 41

> After mass feedback from the public, we're excited to announce that AXLE is switching from Lean to Rocq. The new name will be AXRE (Axiom Rocq Engine). All existing Lean proofs will be automatically translated using GPT-2.

Just saw that, and was thinking, wtf, really? Well... :-)

Print-on-demand Amazon paperback books can have great quality. It is mainly the responsibility of the author, by doing proper layout, and choosing a nice paper option. I've self-published with Amazon KDP, and am really happy with the result.

It can happen that the particular printing person on that day fucks up though.

Just two days ago I was curious about the PhD advisor of my PhD advisor and so on, and discovered that I am actually an academic great-grandson of Hoare (shame on me, I should have realised that earlier), and joked, "Wow, they are all still alive!". Then I saw the news yesterday on HN.

I think that is a very good point. Code is definitely not worthless, but I don't think that capitalism has the right tools for pricing it properly. I think it will become a lot like mathematics in that way.

I see the current generation of AI very much as a thing in between. Opus 4.5 can think and code quite well, but it cannot do these "jumps of insight" yet. It also struggles with straightforward, but technically intricate things, where you have to max out your understanding of the problem.

Just a few days ago, I let it do something that I thought was straightforward, but it kept inserting bugs, and after a few hours of interaction it said itself it was running in circles. It took me a day to figure out what the problem was: an invariant I had given it was actually too strong, and needed to be weakened for a special case. If I had done all of it myself, I would have been faster, and discovered this quicker.

For a different task in the same project I used it to achieve a working version of something in a few days that would have taken me at least a week or two to achieve on my own. The result is not efficient enough for the long term, but for now it is good enough to proceed with other things. On the other hand, with just one (painful) week more, I would have coded a proper solution myself.

What I am looking forward to is being able to converse with the AI in terms of a hard logic. That will take care of the straightforward but technically intricate stuff that it cannot do yet properly, and it will also allow the AI to surface much quicker where a "jump of insight" is needed.

I am not sure what all of this means for us needing to think hard. Certainly thinking hard will be necessary for quite a while. I guess it comes down to when the AIs will be able to do these "jumps of insight" themselves, and for how long we can jump higher than they can.

In principle, this is how these systems work. In practice, there are usually plenty of things that make it difficult to say for sure if you have a proof of something.

You know what? I agree with you. I have not formalised any of my stuff on abstraction logic [1] for that reason (although that would not be too difficult in Isabelle or Lean), I want to write it down in Practal [2], this becoming possible I see as the first serious milestone for Practal. Eventually, I want Practal to feel more natural than paper, and definitely more natural than LaTeX. That's the goal, and I feel many people now see that this will be possible with AI within the next decade.

[1] http://abstractionlogic.com

[2] https://practal.com

Ideas and correctness depend on each other. You usually start with an idea, and check if it is correct. If not, you adjust the idea until it becomes correct. Once you have a correct idea, you can go looking for more ideas based on this.

Formalisation and (formulating) ideas are not separate things, they are both mathematics. In particular, it is not that one should live in Lean, and the other one in blueprints.

Formalisation and verification are not simply certificates. For example, what language are you using for the formalisation? That influences how you can express your ideas formally. The more beautiful your language, the more the formal counter part can look like the original informal idea. This capability might actually be a way to define what it means for a language to be beautiful, together with simplicity.

> Well, assuming it's free of escape hatches like `sorry`

There are bugs in theorem provers, which means there might be "sorries", maybe even malicious ones (depending on what is at stake), that are not that easy to detect. Personally, I don't think that is much of a problem, as you should be able to come up with a "superlean" version of your theorem prover where correctness is easier to see, and then let the original prover export a proof that the superlean prover can check.

I think more of a concern is that mathematicians might not "understand" the proof anymore that the machine generated. This concern is not about the fact that the proof might be wrong although checked, but that the proof is correct, but cannot be "understood" by humans. I don't think that is too much of a concern either, as we can surely design the machine in a way that the generated proofs are modular, building up beautiful theories on their own.

A final concern might be that what gets lost is that humans understand what "understanding" means. I think that is the biggest concern, and I see it all the time when formalisation is discussed here on HN. Many here think that understanding is simply being able to follow the rules, and that rules are an arbitrary game. That is simply not true. Obviously not, because think about it, what does it mean to "correctly follow the rules"?

I think the way to address this final concern (and maybe the other concerns as well) is to put beauty at the heart of our theorem provers. We need beautiful proofs, written in a beautiful language, checked and created by a beautiful machine.

See, I don't get why people say that the world is somehow more complex than the world of mathematics. I think that is because people don't really understand what mathematics is. A computer game for example is pure mathematics, minus the players, but the players can also be modelled just by their observed digital inputs / outputs.

So the world of mathematics is really the only world model we need. If we can build a self-supervised entity for that world, we can also deal with the real world.

Now, you may have an argument by saying that the "real" world is simpler and more constrained than the mathematical world, and therefore if we focus on what we can do in the real world, we might make progress quicker. That argument I might buy.

There is a proof as part of my thesis that the engine is correct, but it is not formal in the sense of machine-checked.

Note that the final result of the Flyspeck project does not depend on that proof, as the linear inequalities part has later on been redone and extended in HOL-Light by Alexey Solovyev, using just the LCF kernel of HOL-Light. Which proves that using a simple LCF kernel can definitely be fast enough for such computations, even on that scale!