practal

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!

As I said, it depends on how you practically implement it.

I've used it for proving linear inequalities as part of the Flyspeck project (formal proof of the Kepler conjecture), and there I implemented my own rewrite engine for taking a set of rewrite rules and do the computation outside of the LCF kernel, for example by compiling the rules to Standard ML. You can view that engine as an extension of the LCF kernel, just one more rule of how to get theorems. In that instance, it is exactly the same.

Yes, indeed, a proof proves what it proves.

You confuse spec and proof.

The basic idea is: You run a program F on some input x, obtain r, and then you have some sort of justification why F x = r is a theorem. There are various levels of how you can do this, one is for example that "running the program" consists of applying a curated set of (proven) rewriting rules that take you from the theorem F x = F x to the theorem F x = r by applying them only to the right hand side. That is basically the same as "Proof by reflection" as used by Gonthier, where the Coq kernel acts as the (unverified) rewriting engine.

So this is not a matter of dependent or static typing or not, the idea is simple and the same (e.g., I've used it for my PhD thesis in Isabelle that is from 2008), it is just a matter of how practical this is to use in your theorem prover of choice.

No, that misunderstands what a proof is. It is very easy to write a SPEC that does not specify anything useful. A proof does exactly what it is supposed to do.

In principle, LLMs can do this already. If you ask Claude to express this in simple words, you will get this translation of the theorem:

    "If applying f to things makes them red whenever they're not already red, then there must exist something that is red AND stays red after applying f twice to it."

You will be able to interact like this, instead of using tactics.

Indeed, and e:t in type theory is quite a strong ontological commitment, it implies that the mathematical universe is necessarily subdivided into static types. My abstraction logic [1] has no such commitments, it doesn't even presuppose any abstractions. Pretty much the only requirement is that there are at least two distinct mathematical objects.

[1] http://abstractionlogic.com

You could, there is no fixed syntax for arrays in Practal, so it would depend on which custom syntax becomes popular. But for expressions that are bracketed anyway, it makes sense to have commas (or other separators), because otherwise you write something like

    [(a b) (x y)]

    [a b, x y]

Sure, color and indentation are optional, but even without those, I don't see that a comma in the above syntax helps much, even on a 80x24 monochrome display. If you want separators, note that the labels which end with a colon are just that, and just as clear as commas. There is a reason why you tried to obfuscate that in your example by placing the colons not with the labels, but the arguments.

Oh, actually that is the syntax I will use for writing abstractions:

    my-abstr x y z foo: "bar" baz: "bak" "quak" quux: [a, b, c, d] lol: 9.7E+42

    my-abstr x y z, foo: "bar", baz: "bak" "quak", quux: [a, b, c, d], lol: 9.7E+42