Hacker News: throw567643u8https://news.ycombinator.com/user?id=throw567643u8Hacker News RSShttps://hnrss.org/hnrss v2.1.1Sat, 05 Sep 2026 06:44:57 +0000<![CDATA[New comment by throw567643u8 in "Formalizing Fermat's Last Theorem"]]>Has Lean proved the Four Colour Theorem? I thought only Rocq had.

]]>Sat, 05 Sep 2026 06:34:49 +0000https://news.ycombinator.com/item?id=49573695throw567643u8https://news.ycombinator.com/item?id=49573695https://news.ycombinator.com/item?id=49573695<![CDATA[New comment by throw567643u8 in "Formalizing Fermat's Last Theorem"]]>AI is hopeless at using existing code, it likes to append only.

]]>Sat, 05 Sep 2026 06:29:54 +0000https://news.ycombinator.com/item?id=49573670throw567643u8https://news.ycombinator.com/item?id=49573670https://news.ycombinator.com/item?id=49573670<![CDATA[New comment by throw567643u8 in "Formalizing Fermat's Last Theorem"]]>With the size of the proof object, a potential buffer overflow comes to mind.

]]>Sat, 05 Sep 2026 06:06:32 +0000https://news.ycombinator.com/item?id=49573533throw567643u8https://news.ycombinator.com/item?id=49573533https://news.ycombinator.com/item?id=49573533<![CDATA[New comment by throw567643u8 in "Formalizing Fermat's Last Theorem"]]>I'd feel so much more excited if this was done in Metamath. Tiny checker kernel, no complicated dependent types, way less to go wrong.

]]>Sat, 05 Sep 2026 01:26:56 +0000https://news.ycombinator.com/item?id=49572173throw567643u8https://news.ycombinator.com/item?id=49572173https://news.ycombinator.com/item?id=49572173<![CDATA[New comment by throw567643u8 in "Formalizing Fermat's Last Theorem"]]>13 million lines of code, a lot of which is new to Mathlib. So it hasn't built on what is already there but synthesised a bunch of new stuff.

LLM generated Lean code in the past has been known to exploit bugs in the Lean kernel, it would be foolish to rule this out happening again.

]]>Sat, 05 Sep 2026 01:16:06 +0000https://news.ycombinator.com/item?id=49572123throw567643u8https://news.ycombinator.com/item?id=49572123https://news.ycombinator.com/item?id=49572123<![CDATA[New comment by throw567643u8 in "Just Bury Your Trash"]]>US centric viewpoints. The UK is running out of space for landfills. Burning it is best for all.

]]>Tue, 01 Sep 2026 21:29:51 +0000https://news.ycombinator.com/item?id=49528511throw567643u8https://news.ycombinator.com/item?id=49528511https://news.ycombinator.com/item?id=49528511<![CDATA[New comment by throw567643u8 in "VulnHunter: Capital One's agentic AI code security tool"]]>Repo will be inactive and obsolete within 12 months.

]]>Sat, 18 Jul 2026 08:43:10 +0000https://news.ycombinator.com/item?id=48956270throw567643u8https://news.ycombinator.com/item?id=48956270https://news.ycombinator.com/item?id=48956270<![CDATA[New comment by throw567643u8 in "Internal Combustion Engine (2021)"]]>Probably better for the environment too.

]]>Wed, 01 Jul 2026 17:07:10 +0000https://news.ycombinator.com/item?id=48750039throw567643u8https://news.ycombinator.com/item?id=48750039https://news.ycombinator.com/item?id=48750039<![CDATA[New comment by throw567643u8 in "Neutron scattering explains why gluten-free pasta falls apart (2025)"]]>> Greg Smith from ISIS as well as collaborators

Didn't know ISIS gave a hoot about gluten free.

]]>Sat, 23 May 2026 05:22:57 +0000https://news.ycombinator.com/item?id=48244965throw567643u8https://news.ycombinator.com/item?id=48244965https://news.ycombinator.com/item?id=48244965<![CDATA[New comment by throw567643u8 in "I have officially retired from Emacs"]]>I know, I tried modal emacs for a while there.

]]>Sun, 03 May 2026 22:07:28 +0000https://news.ycombinator.com/item?id=48002071throw567643u8https://news.ycombinator.com/item?id=48002071https://news.ycombinator.com/item?id=48002071<![CDATA[New comment by throw567643u8 in "I have officially retired from Emacs"]]>Thanks, I left due to rsi from the chords.

]]>Thu, 30 Apr 2026 18:49:32 +0000https://news.ycombinator.com/item?id=47966671throw567643u8https://news.ycombinator.com/item?id=47966671https://news.ycombinator.com/item?id=47966671<![CDATA[New comment by throw567643u8 in "I have officially retired from Emacs"]]>It doesn't have the (any?) diffing capabilities of magit, so it's not usable for me yet.

]]>Wed, 29 Apr 2026 11:50:42 +0000https://news.ycombinator.com/item?id=47947036throw567643u8https://news.ycombinator.com/item?id=47947036https://news.ycombinator.com/item?id=47947036<![CDATA[New comment by throw567643u8 in "I have officially retired from Emacs"]]>I've never found a decent magit replacement since leaving emacs over to vim. There is a Vim attempt at a magit clone, but it is buggy as hell.

]]>Wed, 29 Apr 2026 11:42:46 +0000https://news.ycombinator.com/item?id=47946957throw567643u8https://news.ycombinator.com/item?id=47946957https://news.ycombinator.com/item?id=47946957<![CDATA[New comment by throw567643u8 in "I have officially retired from Emacs"]]>lazygit is too slow for me.

]]>Tue, 28 Apr 2026 21:58:16 +0000https://news.ycombinator.com/item?id=47941415throw567643u8https://news.ycombinator.com/item?id=47941415https://news.ycombinator.com/item?id=47941415<![CDATA[New comment by throw567643u8 in "Category Theory Illustrated – Orders"]]>The author's writing style and overuse of parentheses is excruciating. True parenthetic material is rare, good technical writers use them sparely.

]]>Sat, 18 Apr 2026 15:37:26 +0000https://news.ycombinator.com/item?id=47816732throw567643u8https://news.ycombinator.com/item?id=47816732https://news.ycombinator.com/item?id=47816732<![CDATA[New comment by throw567643u8 in "Category Theory Illustrated – Orders"]]>Just Yoneda Lemma. In fact it feels like the theory just restates Yoneda Lemma over and over in different ways.

]]>Sat, 18 Apr 2026 09:02:54 +0000https://news.ycombinator.com/item?id=47814367throw567643u8https://news.ycombinator.com/item?id=47814367https://news.ycombinator.com/item?id=47814367<![CDATA[New comment by throw567643u8 in "Neovim 0.12.0"]]>With its own package manager now, and LSP library, you really don't need a lot of config tweaking for a minimal vim setup these days.

]]>Sun, 29 Mar 2026 22:05:28 +0000https://news.ycombinator.com/item?id=47567889throw567643u8https://news.ycombinator.com/item?id=47567889https://news.ycombinator.com/item?id=47567889<![CDATA[New comment by throw567643u8 in "Microservices and the First Law of Distributed Objects (2014)"]]>Putting http in between all your components creates a madness machine. Why the cult following around Martin Fowler?

]]>Wed, 25 Mar 2026 17:40:54 +0000https://news.ycombinator.com/item?id=47520689throw567643u8https://news.ycombinator.com/item?id=47520689https://news.ycombinator.com/item?id=47520689<![CDATA[New comment by throw567643u8 in "Wayland set the Linux Desktop back by 10 years?"]]>Does anyone have links on how to set up multi monitor on Sway?

]]>Fri, 20 Mar 2026 04:10:18 +0000https://news.ycombinator.com/item?id=47450390throw567643u8https://news.ycombinator.com/item?id=47450390https://news.ycombinator.com/item?id=47450390<![CDATA[New comment by throw567643u8 in "Duranium: A More Reliable PostmarketOS"]]>Is this a fork, or a change in direction?

]]>Wed, 18 Mar 2026 07:03:11 +0000https://news.ycombinator.com/item?id=47422441throw567643u8https://news.ycombinator.com/item?id=47422441https://news.ycombinator.com/item?id=47422441