Hacker News: tsterin

New comment by tsterin in "Leanstral 1.5"

tsterin — Wed, 01 Jul 2026 05:41:38 +0000

use https://rocq-prover.org/ for that purpose

Show HN: Playbach.io, browser rhythm game (desktop)

tsterin — Wed, 15 Apr 2026 18:43:31 +0000

Article URL: https://playbach.io/

Comments URL: https://news.ycombinator.com/item?id=47783400

Points: 2

# Comments: 0

New comment by tsterin in "[dead]"

tsterin — Thu, 05 Mar 2026 16:40:23 +0000

Opus 4.6 finds proofs of false in Rocq and Lean kernels.

Personal relationship with the bouba-kiki effect

tsterin — Wed, 25 Feb 2026 21:13:11 +0000

Article URL: https://tristan.st/blog/bouba-kiki

Comments URL: https://news.ycombinator.com/item?id=47157936

Points: 5

# Comments: 0

Opus 4.6 is great at formal proofs (Rocq/Lean4)

tsterin — Tue, 17 Feb 2026 15:43:03 +0000

Article URL: https://tristan.st/blog/opus_4_6_formal_proofs

Comments URL: https://news.ycombinator.com/item?id=47048722

Points: 1

# Comments: 0

Let's Start Branching?

tsterin — Sun, 18 Jan 2026 21:19:19 +0000

Article URL: https://branchgpt.netlify.app/

Comments URL: https://news.ycombinator.com/item?id=46672248

Points: 2

# Comments: 0

Spotify leak: why so many 2-minute songs

tsterin — Sat, 27 Dec 2025 16:49:37 +0000

Article URL: https://writingcosmo.substack.com/

Comments URL: https://news.ycombinator.com/item?id=46403061

Points: 2

# Comments: 1

Spotify leak: why so many 2-minute songs

tsterin — Sat, 27 Dec 2025 09:48:26 +0000

Article URL: https://writingcosmo.substack.com/p/the-2m-peak

Comments URL: https://news.ycombinator.com/item?id=46400542

Points: 6

# Comments: 0

The 2m Peak

tsterin — Fri, 26 Dec 2025 18:01:45 +0000

Article URL: https://writingcosmo.substack.com/p/the-2m-peak

Comments URL: https://news.ycombinator.com/item?id=46394459

Points: 1

# Comments: 0

New comment by tsterin in "Determination of the fifth Busy Beaver value"

tsterin — Thu, 18 Sep 2025 11:34:03 +0000

45 minutes on 13 cores on a standard laptop :)

New comment by tsterin in "Determination of the fifth Busy Beaver value"

tsterin — Thu, 18 Sep 2025 08:39:57 +0000

Thank you!

Yeah, one lesson is that if you relax your halting condition to entering a loop at some point you get much longer runtime, see machine Skelet#1 (https://bbchallenge.org/1LC1LE_---1LD_1RD0LD_1LA1RE_0LB0RC), enters a loop after 10^51 steps and the loop is 10^9 steps long.

New comment by tsterin in "Determination of the fifth Busy Beaver value"

tsterin — Thu, 18 Sep 2025 08:38:17 +0000

Thank you!

New comment by tsterin in "Determination of the fifth Busy Beaver value"

tsterin — Thu, 18 Sep 2025 04:48:37 +0000

Best compliment ever

New comment by tsterin in "Determination of the fifth Busy Beaver value"

tsterin — Wed, 17 Sep 2025 14:07:53 +0000

In the paper we mention two other communities which seem to have similar structure and size:

- https://conwaylife.com/, on Conway's GoL and other cellular automata

- Googology, https://googology.fandom.com/wiki/Googology_Wiki and https://googology.miraheze.org/wiki/Main_Page, on big numbers

New comment by tsterin in "Determination of the fifth Busy Beaver value"

tsterin — Wed, 17 Sep 2025 14:03:24 +0000

Number of 5-state TMs is 21^10 = 16,679,880,978,201; coming from (1 + writemovestate)^2*state; difference with your formula is that in our model, halting is encoded using undefined transition.

"essentially different" is not a statically-checked property. It is discovered by the enumeration algorithm (Tree Normal Form, see Section 3 of https://arxiv.org/pdf/2509.12337); in particular, for each machine, the algorithm needs to know it if will ever reach an undefined transition because if it does it will visit the children of that machine (i.e. all ways to set that reached undefined transition).

Knowing if an undefined transition will be ever reached is not computable, hence knowing the number of enumerated machines is not computable in general and is as hard as solving BB(5).

New comment by tsterin in "Determination of the fifth Busy Beaver value"

tsterin — Wed, 17 Sep 2025 13:24:32 +0000

In Coq-BB5 machines are not run for 100M steps but directly thrown in the pipeline of deciders. Most halting machines are detected by Loops using low parameters (max 4,100 steps) and only 183 machines are simulated up to 47M steps to deduce halting.

In legacy bbchallenge's seed database, machines were run for exactly 47,176,870 steps, and we were left with about 80M nonhalting candidates. Discrepancy comes from Coq-BB5 not excluding 0RB and other minor factors.

Also, "There are 181 million ish essentially different Turing Machines with 5 states", it is important to note that we end up with this number only after the proof is completed, knowing this number is as hard as solving BB(5).

New comment by tsterin in "ZenGPT: Hide ChatGPT's Typing, Show Only Final Answer"

tsterin — Tue, 09 Sep 2025 16:00:56 +0000

Repeatedly watching ChatGPT stream out words was giving me a headache, so I built ZenGPT: it hides responses until they’re fully generated.

https://chromewebstore.google.com/detail/zengpt/jcmppahlhehi... https://github.com/tcosmo/zengpt

ZenGPT: Hide ChatGPT's Typing, Show Only Final Answer

tsterin — Tue, 09 Sep 2025 16:00:56 +0000

Article URL: https://chromewebstore.google.com/detail/zengpt/jcmppahlhehiaoknhgjoojncbgagggik

Comments URL: https://news.ycombinator.com/item?id=45183918

Points: 3

# Comments: 1

New comment by tsterin in "BB(3, 4) > Ack(14)"

tsterin — Thu, 23 May 2024 18:58:36 +0000

I really like your point (I'm one of bbchallenge maintainers). I think that Discord is close to optimal for us in the short term, but bad for the reasons you and other have mentioned mid/long term.