Hacker News: Gehinnn

New comment by Gehinnn in "Postmortem for Kernel Soundness Bug #14576"

Gehinnn — Sun, 02 Aug 2026 08:00:58 +0000

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.

New comment by Gehinnn in "Postmortem for Kernel Soundness Bug #14576"

Gehinnn — Sat, 01 Aug 2026 22:41:27 +0000

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.

New comment by Gehinnn in "EEG shows brain can simultaneous encode two speech streams"

Gehinnn — Fri, 17 Jul 2026 09:18:49 +0000

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

New comment by Gehinnn in "Google copybara: moving code between repositories"

Gehinnn — Wed, 01 Jul 2026 08:23:43 +0000

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.

New comment by Gehinnn in "Twenty One Zero-Days in FFmpeg"

Gehinnn — Fri, 12 Jun 2026 23:13:59 +0000

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?

New comment by Gehinnn in "Lean 4: How the theorem prover works and why it's the new competitive edge in AI"

Gehinnn — Sat, 21 Feb 2026 23:30:52 +0000

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.

New comment by Gehinnn in "Lean 4: How the theorem prover works and why it's the new competitive edge in AI"

Gehinnn — Sat, 21 Feb 2026 14:36:37 +0000

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

New comment by Gehinnn in "Lean 4: How the theorem prover works and why it's the new competitive edge in AI"

Gehinnn — Sat, 21 Feb 2026 14:32:46 +0000

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)

New comment by Gehinnn in "Lean 4: How the theorem prover works and why it's the new competitive edge in AI"

Gehinnn — Sat, 21 Feb 2026 10:31:30 +0000

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.

New comment by Gehinnn in "Testing Ads in ChatGPT"

Gehinnn — Mon, 09 Feb 2026 19:30:38 +0000

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)

New comment by Gehinnn in "The silent death of good code"

Gehinnn — Sun, 08 Feb 2026 00:56:35 +0000

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.

New comment by Gehinnn in "Project Genie: Experimenting with infinite, interactive worlds"

Gehinnn — Fri, 30 Jan 2026 10:12:57 +0000

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.

New comment by Gehinnn in "Ask HN: How do I help a colleague who introduces a lot of typos?"

Gehinnn — Fri, 02 Jan 2026 08:46:47 +0000

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

New comment by Gehinnn in "Show HN: Minimalist editor that lives in browser, stores everything in the URL"

Gehinnn — Wed, 24 Dec 2025 23:28:28 +0000

This is very cool!

New comment by Gehinnn in "I Learned the Pythagorean Theorem"

Gehinnn — Sun, 23 Nov 2025 23:31:07 +0000

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?

New comment by Gehinnn in "Bach Cello Suites (2024)"

Gehinnn — Thu, 25 Sep 2025 21:16:10 +0000

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

New comment by Gehinnn in "Do the simplest thing that could possibly work"

Gehinnn — Sat, 30 Aug 2025 08:26:10 +0000

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

New comment by Gehinnn in "Why LLMs can't really build software"

Gehinnn — Thu, 14 Aug 2025 19:15:50 +0000

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.

New comment by Gehinnn in "The Anti-Pattern Game"

Gehinnn — Wed, 13 Aug 2025 14:39:17 +0000

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.

New comment by Gehinnn in "The Anti-Pattern Game"

Gehinnn — Wed, 13 Aug 2025 10:27:05 +0000

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?