Using "length of the correctness statement + length of its proof" works quite well as proxy for complexity of a component (the longer, the more complex).
Copy pasted functions with subtle changes mean you cannot reuse the proof (DRY). Giant functions with lots of if/else statements however might cause a branch explosion in the proof. The right abstraction removes lots of assumptions that a proof could depend on, limiting the search space and often forcing elegance (this also applies to math, eg. when reasoning with abstract groups instead of integers).
The wrong abstraction might force case distinctions on consumers of the abstraction.
> Using "length of the correctness statement + length of its proof" works quite well as proxy for complexity of a component (the longer, the more complex).
It sounds like a reasonable concept, but then Principia Mathematica takes 300 pages to prove that 1+1 is 2.
I'd love to be able to flash a custom firmware on the withings body+ to make the screen truly smart. It's a bummer to know that AI can do all these things if only the firmware was open source / accessible.
Same. It annoys me I cannot use baby wright mode to also weigh my dog as she's heavier than the 5kg limit they impose. However, reverse engineering firmware is really easy these days...
Has there ever been a bug that allowed to prove a previously unproven statement, without allowing the user to prove "false" by exploiting the bug directly?
If every bug-exploiting proof would make it easy to prove false, putting a bounty on proving false could increase trust in the validity of verified but obscure Lean proofs.
We want Lean4 (or any other deduction system that we use, for that matter) to be correct, i.e. "what is a true statement" and "what is a derivable statement" should be the same.
"every statement that can be derived also holds" is the difficult part to show, and something we refer to as soundness. For some fancy logics, it's not even possible to show, hence the discovered Kernel Soundness Bug in Lean!
"every statement that holds can also be derived", a notion known as completeness, is often a trivial property; in practice, we use refutation completeness instead, i.e. "every statement that doesn't hold can derive false". A bug that would allow a user to prove/derive a previously unproven statement would fall under this category of "completeness bug".
However, such completeness bugs immediately show up in testing. Generally, deduction systems have two kinds of rules: a handful of rules that are enough to establish (refutation) completeness, and then a few extra rules to optimize inference. Because so few rules are needed for completeness, lots of test cases will break if one of the rules break.
--
I'm not actually sure how the completeness situation looks like for proper provers like Lean. It's my graduate student's hubris to assume completeness remains easy to show for more advanced systems than the Superposition calculus ;)
>"what is a true statement" and "what is a derivable statement" should be the same.
you mention completeness in the rest of your comment, so I'm not sure how you aren't aware of this, but the famous incompleteness theorem says that for a consistent set of axioms there will always be true statements you can't prove.[1]
That's not what it says. It says that as long as the logic is rich enough (first-order isn't enough) and consistent there are statements where neither the statement nor its negation is provable. You may choose to create a new logic by adding either the statement or its negation as an additional axiom, and it will (obviously?) remain consistent.
Truth is some sort of value judgment that is outside the scope of formal systems. And looking at how bizarre Gödel statements are, it's unclear if there's any particular justification for declaring them to be true or false.
The second paragraph of my link talks specifically about truth:
>The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.e. an algorithm) is capable of proving all truths about the arithmetic of natural numbers. For any such consistent formal system, there will always be statements about natural numbers that are true, but that are unprovable within the system.
You can make it complete, it just won't be consistent.
In fact there is a simple way to do it -- add contradictory axioms and then you can use the principle of explosion to prove any statement as true. Is such a system inconsistent and thus useless? Yes, but it is complete.
Don't Godel's incompleteness theorems mean that completeness is a property you don't want in a prover (as it means the prover must then be inconsistent and this unsuable) and consistency is a property of the prover you cannot prove using the prover itself?
Not necessarily. For example, perhaps my ZFC first-order-logic theorem checker implicitly accidentally contains the continuum hypothesis as an axiom. This isn't inconsistent but it is a correctness bug.
(For that matter, another correctness bug is "the checker rejects all proofs". You can't prove false if you can't prove anything.)
But how obvious would that be in the proof? Especially when you don't know if the proven statement is not true/implies false.
Afaik all past problematic Lean bugs clearly implied false. But could it be that a bug is used in a way that this is absolutely not clear?
For example, the bug could allow proving a=b if the hashes of the terms equal. And the only (hypothetically) known hash collision that could be used to exploit this might not lead to an obvious contradiction.
Let a and b be as you describe (hash collision), and suppose that collisions are extremely rare. We have a theorem that a=b => a+1=b+1. But in this case, a=b according to our hash-equality, but a+1!=b+1, which contradicts the theorem we've already proved.
for real problems with my statement, see your sibling comment.
One of the first ways I learned to meditate/access different states of mind was a technique described as "overload trance" (IIRC). The premise was, listen to a piece of music, focusing on one musical component, then while keeping that focus, add another element, and another, etc.
It works best with pieces with a lot of ostinato (repetition/vamp) and Bach's Little Fugue in G minor was and is one of my favorites. Really fun to play too, though i get tripped up as soon as the feet get involved. Also, Utopia by Astral Projection (that whole album Trust in Trance 3 is great for this).
Bonus points to mentally visualizing something in time with the music (I like orbs whirling around like atomic orbitals). You can really tie up much of your mental processing this way and I find it much easier than traditional zen meditation, trying to bring focus back to eg. breathing.
Does this tool allow changes in both repositories? (with a 3 way merge strategy)
git subtrees come close, but I have a use case where I need transformations/file filters on top.
What do you mean "video file that I'm perfectly willing to play in my browser". Isn't it safe to assume that no video file can escape the browser decoding sandbox?
I'm not up-to-speed with the current state of sandboxing in browsers, but in principle it's (on modern operating systems) not especially hard for them to sandbox the decoding into a separate process with basically no privileges beyond rendering a video stream. It's a bit trickier if we're only considering demuxing and delegating decoding to the hardware, but that's a much smaller attack surface.
A manually run ffmpeg on the command line does nothing to restrict its privileges, and its security model has very little interest in doing so, while browsers very much have.
I just completed the formal verification of my bachelor thesis about real time cellular automata with Lean 4, with heavy use of AI.
Over the past year, I went from fully manual mode (occasionally asking chat gpt some Lean questions) to fully automatic mode, where I barely do Lean proofs myself now (and just point AI to the original .tex files, in German).
It is hard to believe how much the models and agentic harnesses improved over the last year.
I cannot describe how much fun it is to do refactorings with AI on a verified Lean project!
Also, it's so easy now to have visualizations and typesetted documents generated by AI, from dependency visualizations of proofs using the Lean reflection API, to visual execution traces of cellular automatas.
I use VS Code in a beefy Codespace, with GitHub Copilot (Opus 4.5).
I have a single instruction file telling the AI to always run "lake build ./lean-file.lean" to get
feedback.
This is very similar to how I worked with Lean a year ago (of course in a much simpler domain) - mostly manual editing, sometimes accepting an inline completion or next edit suggestion.
However, with agentic AI that can run lean via CLI my workflow changed completely and I rarely write full proofs anymore (only intermediate lemma statements or very high level calc statements).
There have been bugs in Lean that allowed people to prove False, from which you can prove anything (they have been fixed).
Otherwise, if you check that no custom axiom has been used (via print axioms), the proof is valid.
It's easy to construct such an example: Prove that for all a, b, c and n between 3 and 10^5, a^n=b^n+c^n has no solution.
The unmeaningful proof would enumerate all ~10^20 cases and proof them individually. The meaningful (and probably even shorter) proof would derive this from Fermat's theorem after proving that one.
Forget about that, the founders literally said word for word that advertising ruins search quality in their seminal paper. They became the exact thing they fore-warned about their competitors at the time.
Down-right joke really. The people who idolise them are incredibly delusional.
lol pretty much. their reservation price was more than met.
Although considering Brin's interactions with female employees etc, no surprise really. They were full of it from the off. Page is better at hiding it.
Opus is quite good at refactoring. Also, we can finally have all the helper functions/beautiful libraries/tests that we always wanted to have. There is no excuse anymore to approximate a parser with regular expressions.
Or to not implement the adapter class which makes an ugly unchangeable interface beautiful.
I believe the right use of AI makes it possible to write more beautiful code than ever before.
I would be extremely happy to be proven wrong! I love using agents for exploratory prototypes as well as "rote" work, but have yet to see them really pay off when dealing with existing tech debt.
I find that the flaws of agentic workflows tend to be in the vein of "repeating past mistakes", looking at previous debt-riddled files and making an equivalently debt-riddled refactor, despite it looking better on the surface. A tunnel-vision problem of sorts
Copy pasted functions with subtle changes mean you cannot reuse the proof (DRY). Giant functions with lots of if/else statements however might cause a branch explosion in the proof. The right abstraction removes lots of assumptions that a proof could depend on, limiting the search space and often forcing elegance (this also applies to math, eg. when reasoning with abstract groups instead of integers). The wrong abstraction might force case distinctions on consumers of the abstraction.
reply