Gehinnn

5 ms·

1.
by Gehinnn 10d ago
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 (D
2.
by Gehinnn 10d ago
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.
3.
by Gehinnn 2mo ago
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
4.
by Gehinnn 2mo ago
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
5.
by Gehinnn 2mo ago
I believe this is why fugues are such a pleasure to listen to!
6.
by Gehinnn 3mo ago
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.
7.
by Gehinnn 3mo ago
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?
8.
by Gehinnn 7mo ago
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
9.
by Gehinnn 7mo ago
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
10.
by Gehinnn 7mo ago
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: ht
11.
by Gehinnn 7mo ago
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 full
12.
by Gehinnn 7mo ago
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)
13.
by Gehinnn 7mo ago
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
14.
by Gehinnn 8mo ago
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 t
15.
by Gehinnn 9mo ago
Most editors have some kind of spelling mistake linting extension, that should help!
16.
by Gehinnn 9mo ago
This is very cool!
17.
by Gehinnn 10mo ago
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 me
18.
by Gehinnn 1y ago
I wish Spotify would allow me to easily compare the same classical pieces with different recordings!
19.
by Gehinnn 1y ago
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 restructu
20.
by Gehinnn 1y ago
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
21.
by Gehinnn 1y ago
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.
22.
by Gehinnn 1y ago
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?
23.
by Gehinnn 1y ago
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 repetiti
24.
by Gehinnn 1y ago
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)
25.
by Gehinnn 1y ago
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?
26.
by Gehinnn 1y ago
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 a
27.
by Gehinnn 1y ago
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 r
28.
Updating the Criteria for Web API Extended Access(developer.spotify.com)
1 points by Gehinnn 1y ago|0 comments
29.
by Gehinnn 1y ago
But how do you make sure the user actually runs your component without any modification?
30.
by Gehinnn 1y ago
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 )

More ›