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.
> 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.
> 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 this is sort of how lean itself already works. It has a minimal trusted kernel that everything is forced through. Only the kernel has to be verified.
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.
Understanding IMO is "developing a correct mental model of a concept".
Some heuristics of correctness:
Feynman: "What I cannot build. I do not understand"
Einstein: "If you can't explain it to a six year old, you don't understand it yourself"
Of course none of this changes anything around the machine generated proofs. The point of the proof is to communicate ideas; formalization and verification is simply a certificate showing that those ideas are worth checking out.
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.
I share your fascination with proof assistants and formal verification, but the reality is that I am yet to see an actual mathematician working on frontier research who is excited about formalizing their ideas, or enthusiastic about putting in the actual (additional) work to build the formalization prerequisites to even begin defining the theorem's statement in that (formal) language.
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.
>I am yet to see an actual mathematician working on frontier research who is excited about formalizing their ideas
British mathematician Kevin Buzzard has been evangelizing proof assistants since 2017. I'll leave it to you to decide whether he is working on frontier research:
Sure, he is one of biggest advocates for it, and yet he was quite clear that it is not yet possible for him to do his actual research in Lean.
Quoting one of the recent papers (2020):
> With current technology, it would take many person-decades to formalise Scholze’s results. Indeed,
even stating Scholze’s theorems would be an achievement. Before that, one has of course to formalise
the definition of a perfectoid space, and this is what we have done, using the Lean theorem prover.
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.
> 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.
In theory I think you are kind of right, in that you can model a lot of real world behaviour using maths, but it's an extremely inefficient lense to view much of the world through.
Consider something like playing catch on a windy day. If you wanted to model that mathematically there is a lot going on: you've got the ball interacting with gravity, fluid dynamics of the ball moving through the air, the changing wind conditions etc. yet this is a very basic task that many humans can do without really thinking about it.
Put more succinctly, there are many things we'd think of as very basic which need very complex maths to approach.
This view of simulation is just wrong and does not correspond at all to human perception.
Firstly, games aren't mathematics. They are low quality models of physics. Mathematics can not say what will happen in reality, mathematics can only describe a model and say what happens in the model. Just mathematics can not say anything about the real world, so a world model just doing mathematics can not say anything about the world either.
Secondly, and far worse for your premise, is that humans do not need these mathematical models. I do not understand the extremely complex mechanical problem of opening a door, to open a door. A world model which tries to understand the world based on mathematics has to. This makes any world model based on mathematics strictly inferior and totally unsuited to the goals.
The world of mathematics is only a language. The (Platonic) concepts go from simple to very complex, but at the base stands a (dynamic and evolving) language.
The real world however is far more complex and perhaps rooted in a universal language, but in one we don’t know (yet) and ultimately try to describe and order by all scientific endeavors combined.
This philosophy is an attempt to point out that you can create worlds from mathematics, but we are far from describing or simulating ‘Our World’ (Platonic concept) in mathematics.
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.
> That is basically the same as "Proof by reflection" as used by Gonthier, where the Coq kernel acts as the (unverified) rewriting engine.
I don't think it's "basically the same", because this application of the rewrite rules in a LCF-like system is explicit (i.e. the proof checking work grows with the size of the problem), while in proof by reflection in a type theory it happens implicitly because the "rewriting" happens as part of reduction and makes use of with the definitional equality of the system?
For small and medium examples this probably doesn't matter, but I would think that for something like the four colour theorem it would.
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.
How does the proof of correctness work in this case? Is the rewriting ultimately resorting to proof steps within the kernel like a LCF-tactic would, or is there simply an informal argument that whatever you're doing in the rewriter is correct, on par with the proof kernel itself?
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!
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.
No, a proof proves what it proves. It does not prove what the designer of the proof intended it to prove unless the intention and the proof align. Proving that is outside of the realm of software.
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."
Now the proof is easy to see, because it is the first thing you would try, and it works: If you have a red thing x, then either x and f(f(x)) are both red, or f(x) and f(f(f(x)) are both red. If x is not red, then f(x) is red. Qed.
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.
While I have no problems with indentation based syntax, it's not very conductive to minimization, so it's a no go for JSON's case.
Coloring things is a luxury, and from my understanding not many people understand that fact. When you work at the trenches you see a lot of files on a small viewport and without coloring most of the time. Being able to parse an squiggly file on a monochrome screen just by reading is a big plus for the file format in question.
As technology progresses we tend to forget where we came from and what are the fallbacks are, but we shouldn't. Not everyone is seeing the same file in a 30" 4K/8K screen with wide color gamut and HDR. Sometimes a 80x24 over some management port is all we have.
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.
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
reply