Gehinnn

I believe this is why fugues are such a pleasure to listen to!

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?

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.

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

Here is a session that I just had with AI: https://gist.github.com/hediet/e3569a7c6b4b7c4f7d4a7db410104... (summarized by AI).

And here are some examples of the different philosophies of AI proofs and human proofs: https://gist.github.com/hediet/e3569a7c6b4b7c4f7d4a7db410104...

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.

(disclaimer: I work on VS Code)

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.

The ads in Google also started like this. (However, to my knowledge, there is no way I can pay Google to get the ads in my search removed)

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.

Doesn't this have some implications for P vs NP?

How much compute do you need to convince a brain its environment is "real"?

What happens if I build a self replicating super computer in this environment that finds solutions to some really big SAT instances that I can verify?

Dreams run into contradictions quite quickly.

Most editors have some kind of spelling mistake linting extension, that should help!

This is very cool!

I still have difficulties understanding on a high level why lengths in triangles can produce irrational numbers. I guess once you accept that area in two dimensions involves multiplication, it is a necessary consequence.

I wonder what it means for projects such as wolfram physics where space is discrete. Do truly right angled triangles even exist in nature?

I wish Spotify would allow me to easily compare the same classical pieces with different recordings!

Is doing a refactoring ever the simplest thing that could have been done? I think "do the simplest thing" should be "do the thing that increases complexity the least" (which might be difficult to do and require restructuring).

I wouldn't say "translating", but "finding/constructing a model that satisfies the business rules". This can be quite hard in some cases, in particular if some business rules are contradicting each other or can be combined in surprisingly complex ways.

Just checked with AI: Thue showed 1906 that there are infinitely many square free words (:= a word that doesn't contain a non-primitive word) over an alphabet with at least 3 symbols.

Yes, seems like there are only finitely many words over a binary alphabet that do not contain a non-primitive word (0, 01, 010 and 1, 10, 101). How would it change if the alphabet has three symbols?

This reminds me of primitive words [1]: A primitive word is a word that is not the (2+ times) repetition of any other word. This is slightly different than a non-pattern word from the article, which is a word that is not a 3+ times repetition of any other word.

The anti-pattern game is about extending words such that they do not contain a pattern word.

I wonder how the situation changes if 2 times repetitions would count as pattern (i.e. non-primitive words).

For primitive words, it is an open problem if the language of primitive words (over any non-trivial finite alphabet) is context free.

I wonder if the language of words that don't contain patterns (or non-primitive words) is context free.

[1] https://arxiv.org/abs/1104.4427

Does this mean that most of the proofs in Lean and LeanQ would look exactly the same, it's just that the proofs of some technical low-level lemmas around quotient types (which I guess mathematicians are not really interested in anyway) look different?

For example, if I want to prove that a+b=b+a, I wouldn't care if I'm directly in peano arithmetic or just have a construction of the peano axioms in ZFC, as in both cases the proofs would be identical (some axioms in PA would be lemmas in ZFC).

If that's the case with quotients, I wonder why it's such a big deal for some.

How much does this leak into typical math-related proofs? If someone would create LeanQ where quotient types are built in nicely, how much work would it be to port the Fermat project from Lean to LeanQ?

The impossible chess board problem must have something to do with the idea of solving tree eval with little memory (https://youtu.be/wTJI_WuZSwE?si=lgTc65RhXQesKchR)! When the chess board is random, it feels impossible to add additional information. However, by choosing which cell to flip and knowing that you followed a certain operation, you can encode the position information in the random data, without needing more cells.

This would be the classical proof via strong induction, without Σ-types:

https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAZRgEwHQBECGN...

Doing the proof inside the algorithm (i.e. doing inline induction over the algorithm recursion structure) has the advantage that the branching structure doesn't have to be duplicated as in an external proof like the one I did.

In my proof I didn't struggle so much with induction, but much more with basic Lean stuff, such as not getting lost in the amount of variables, dealing with r.fst/r.snd vs r=(fst, snd) and the confusing difference of .get? k and [k]?.

But how do you make sure the user actually runs your component without any modification?

Would be nice if it could use the Accessibility Tree from chrome dev tools to navigate the page instead of relying on screenshots (https://developer.chrome.com/blog/full-accessibility-tree)

You could say the same about art. Artists put lots of time and effort into creating unuseful things to inspire others. Just like here!

A nice property of monoids is associativity, which allows for some interesting incremental algorithms, e.g. by using balanced trees: If the fold of × on a list is computed in clever way, the fold of × on a list where one element is modified can be computed in logarithmic time, given the computation of the first list.

A good example for a monoid are strings with the string concatenation operation! This is used a lot in text editors. Homomorphisms are also of practical relevance here.

If × is a commutative group operation (i.e. inverse elements exist and a×b=b×a), that can even be done in constant time in a trivial way.

A good abstraction shouldn't make its usage shorter, it should make the proof that the usage is correct shorter.

This usually means the total amount of assumptions needed to prove everything correct is decreased. (when the code is not actually formally verified, think of "proof length" as mental capacity needed to check that some unit of code behaves as intended)

I think the primary change is that these debates were focused on producing diffs that humans read; now the debate is whether the algorithms can accomplish this result with no human involvement at all.

The better the diff captures the intent of the user change, the easier the diff is to read, AND it also becomes easier to understand merge conflicts, as the conflict becomes a conflict of intents and not characters. Sometimes certain conflicts can even be avoided if the diffs are chosen right (or are expressive enough, e.g. when code moves can be detected).

I'd pay a lot per month if I wouldn't have to care which subscriptions I need and could just access everything.

I wouldn't pay a lot for any particular service that I'd just use only once or twice per month. I only ever read "the verge" if it is linked from HN or somewhere else. A subscription just doesn't make sense for me.