Viewing profile — Gehinnn

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 f…

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 …

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 use…

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 sugges…

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 philosoph…

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 mod…

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 approxi…

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 comput…

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 multip…

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 …

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 c…

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 symbo…

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 …

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 …

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 gu…

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 proje…

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 ch…

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