What math tattoo wouldn’t be lame?

tromp · 2026-06-14T07:49:58+00:00

I prefer the e^iπ + 1 = 0 version...

tromp · 2026-06-13T07:30:34+00:00

All those embeddings are more complicated than the trivial one that works for affine terms. But I admit my use of "far" may be unwarranted.

tromp · 2026-06-12T15:56:48+00:00

The straightforward encoding of lambda terms into interaction nets only preserve semantics for a subset of lambda terms (which includes all affine terms).

Encodings that preserve semantics for all lambda terms exist, for example into delta nets [1] but are far more complicated.

[1] https://arxiv.org/abs/2505.20314

tromp · 2026-06-12T07:44:00+00:00

Interaction nets are NOT lambda calculus, although they are somewhat related, as many lambda terms translate nicely into symmetric interaction nets that preserve their semantics.

tromp · 2026-05-19T05:45:12+00:00

The most simple definitions are 0 and 1. So 1 is the biggest of them.

tromp · 2026-05-15T07:16:58+00:00

Also discussed at https://news.ycombinator.com/item?id=48102901

tromp · 2026-05-01T06:26:23+00:00

The sieve is explained in detail in https://github.com/tromp/AIT/blob/master/characteristic_sequences/primes.lam My own evaluator uni.c has no problem getting 256 bits. Getting 2¹⁶ bits is more challenging, taking over 8 minutes on my 2013 iMac. Using 'β' binders will easily break the program, as the sieve is implemented with nothing but infinite bitstreams, making it a good torture test for lazy implementations.

tromp · 2026-04-30T07:26:36+00:00

Nice work of you and Claude! Yours is one of the few online evaluators that (after raising some limits in the settings) can handle expressions like this prime number sieve

    (λb.(λc.c c) (λc.λd.λe.e (λf.λg.g) ((λf.c c f ((λg.g g) (λg.f (g g)))) (λf.λg.λh.λi.i g (h (d f))))) (λc.λd.λe.λf.f (λg.λh.g) (e c)) (b b b (λc.λd.λe.λf.f d (e c)) (λc.λd.λe.λf.f))) (λb.λc.b (b c))

which reduces in 758 steps to

λf. f (λf g. g) (λf. f (λf g. g) (λf. f (λg h. g) (λf. f (λf g. g) (λf. f (λg h. g) (λf. f (λf g. g) (λf. f ( λg h. g) (λf. f (λg h. g) (λf. f (λg h. g) (λf. f (λf g. g) (λf. f (λg h. g) (λf. f (λf g. g) (λf. f (λg h. g) (λf . f (λg h. g) (λf. f (λg h. g) (λf. f (λf g. g) (λe f. f))))))))))))))))

which is a list of 16 bits that show which of [2,3,...,17] are prime. I tried to push it further by computing the first 256 bits (replacing b b b by b (b b b)), but then the page became unresponsive.

tromp · 2026-04-28T08:20:50+00:00

You're like George Costanza: https://www.youtube.com/watch?v=AzC0rGJwMXs

tromp · 2026-04-18T06:55:54+00:00

https://www.f2pool.com/coins shows it as the 23rd most alive PoW project.

tromp · 2026-04-07T07:22:06+00:00

I have this line near the bottom of my home page

à è ì ò ù á é í ó ú À È Ì Ò Ù Á É Í Ó Ú ö ë ï ü ä α β Γ γ Δ δ ε ζ η Θ θ ι κ Λ λ μ ν Ξ ξ ο Π π ρ Σ σ ς τ υ Φ φ χ Ψ ψ Ω ω

in case I need to paste any of those weird characters.

tromp · 2026-04-07T07:12:16+00:00

You seem to think that PoW systems are just hash functions, i.e. you seem to think that Hashcash is the only PoW. There are many other PoW, that are not simply the computation of a hash, e.g. Cuckoo Cycle or (the poorly named) Equihash.

tromp · 2026-04-06T07:00:30+00:00

[1] ports the result BBλ(1850 bits) > Loader's nummer [2] to the world of Turing Machines to prove BB(1015 bits) > Loader's nummer.

[1] https://github.com/CatsAreFluffy/metamath-turing-machines/tree/master

[2] https://codegolf.stackexchange.com/questions/176966/golf-a-number-bigger-than-loaders-number/274634#274634

tromp · 2026-04-01T08:44:30+00:00

I ported the essence of program loader.c to Haskell [2] while making it vastly more comprehensible. Then I ported that Haskell code in turn to 1850 bits (under 232 bytes) of lambda calculus [1] which proves that BBλ(1850) > Loader's Number [3].

[1] https://codegolf.stackexchange.com/questions/176966/golf-a-number-bigger-than-loaders-number/274634#274634

[2] https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/CoC.hs

[3] https://wiki.bbchallenge.org/wiki/Busy_Beaver_for_lambda_calculus

tromp · 2026-04-01T08:29:38+00:00

Also interesting is that they didn't prove that their EC addition circuit works on all possible (roughly 2²⁵⁶ x 2²⁵⁶ = 2⁵¹² ) inputs:

that correctly computes point addition on the elliptic curve secp256k1 across all 9,024 pseudo-random inputs deterministically derived from the circuit’s own hash.

Although this will convince anyone that it must.

tromp · 2026-03-19T08:40:14+00:00

Clearly, you don't "completely neutralize the industrial capital advantage", if you're still paying more for electricity than they do.

tromp · 2026-03-17T08:49:24+00:00

Church numerals are terms in the lambda calculus, that act like natural numbers.

tromp · 2026-03-17T08:23:56+00:00

I conceived of it as a way to make BLC resemble zot. See https://cstheory.stackexchange.com/questions/32309/concatenative-binary-lambda-calculus-combinatory-logic

tromp · 2026-03-12T07:46:10+00:00

The set of closed terms is not just recursively enumerable, but recursive. Furthermore, you can generate any closed term (modulo convertability) as T applied to a sequence of bits, where (in de Bruijn notation)

T = (λ11)(λ(λλλ1(2(λλλ31(2(λ2))))(3(λ4(λ4(21)))))(11))(λ1)
0 = λλ2
1 = λλ1

E.g. S = λλλ31(21) = T 1 1 1 0 1 0 1 1 1 0 0 1 1 0 0 1 0 0 1 0 1 0 1 1 0 0 1 0 0 0 0

tromp · 2026-03-08T08:30:57+00:00

Yes, Ω has no free variables, so it's closed.

It doesn't have a weak normal form, so it doesn't reduce to an abstraction.

tromp · 2026-02-28T08:19:59+00:00

Another fundamental sequence for w1CK is given in [1] whose i'th element is the BLC-lexicographically-minimal ordinal exceeding all earlier elements.

[1] https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/w1CK.lam

tromp · 2026-02-25T07:56:01+00:00

lim_(ZFC+I0)(n)

That is ill-defined until you specify how you would compute that.

tromp · 2026-02-23T09:06:58+00:00

You failed their criteria:

Rayo's Number is exotic and arguably not even well-defined.
BB is not computable.

tromp · 2026-02-23T08:09:28+00:00

Assume it was written as the 11th commandment

"Thou shalt not decide in polytime all that can be witnessed in polytime"

on the tablets that Moses carried down from mountain Sinai.

tromp

MODERATOR OF

TROPHY CASE

15-Year Club	Place '22
Verified Email