RE: https://mastodon.social/@lobsters/116002869083328549

#maths #mathematics #number #NumberTheory #computation #BusyBeaver #LambdaCalculus #LargeNumbers
https://tromp.github.io/blog/2026/01/28/largest-number-revised

Propositions As Types Analogy • 1
• https://inquiryintoinquiry.com/2013/01/29/propositions-as-types-analogy-1/

One of my favorite mathematical tricks — it almost seems too tricky to be true — is the Propositions As Types Analogy. And I see hints the 2‑part analogy can be extended to a 3‑part analogy, as follows.

Proof Hint ∶ Proof ∶ Proposition
∷
Untyped Term ∶ Typed Term ∶ Type

or

Proof Hint ∶ Untyped Term
∷
Proof ∶ Typed Term
∷
Proposition ∶ Type

See my working notes on the Propositions As Types Analogy —
• https://oeis.org/wiki/Propositions_As_Types_Analogy

#Mathematics #CategoryTheory #ProofTheory #TypeTheory
#Logic #Analogy #Isomorphism #PropositionalCalculus
#CombinatorCalculus #CombinatoryLogic #LambdaCalculus
#Peirce #LogicalGraphs #GraphTheory #RelationTheory

What Is Control Flow Analysis for Lambda Calculus? – Iowa Type Theory Commute

https://rss.buzzsprout.com/728558.rss

#HackerNews #ControlFlowAnalysis #LambdaCalculus #TypeTheory #IowaCommute #HN

I've been working through Type Theory & Formal Proof.

Why? I was curious as to how proof assistants like Lean worked. Someone recommended it.

Is it any good? I think the book is excellent. It provides a gentle ramp from no previous knowledge to the basics of lambda calculus and some extensions, and the central idea of propositions as types / proofs as terms. The exercises are well calibrated. Of course nothing is perfect but this is far better than most texts I've suffered through.

I'm self-teaching so there is a chunky risk my errors and misunderstandings go uncaught... but I'm writing up my solutions in case others find them useful. Writing them publicly also pushes up my own quality threshold from scribbles in a notepad to something more thought through.

https://type-theory-and-formal-proof.blogspot.com

#maths #typetheory #lambdacalculus #proofassistants

beginner question:

when we say " assume 𝐴:* "

does this mean " assume ∅;∅ ⊢ 𝐴:* " ?

intuitively this makes sense, seems almost obvious, but I'm trying to root my intuitions in actual derivation rules, here λ𝐷₀

---

as background I'm a beginner self-teaching his stuff, and right now my brain is a bit wobbly around whether something being true in an empty context is always true in an arbitrary context (which doesn't seem true to me, because the context can contradict the assertion)

#typetheory #lambdacalculus

Been struggling with this for days... help!

If 𝑋:𝑌 is derivable in the empty context, that is

∅ ⊢ 𝑋:𝑌

this is it always true that :

(i) 𝑋:𝑌 is derivable in any context as long as it doesn't "override" anything in 𝑋 or 𝑌 ?

Γ ⊢ 𝑋:𝑌

(ii) 𝑋:𝑌 is derivable in any context + any environment as long as they don't "override" anything in 𝑋 or 𝑌 ?

Δ;Γ ⊢ 𝑋:𝑌

#typetheory #lambdacalculus

I'm not understanding this intuitively.

I can't think of examples of a formal definition (in λD) that are NOT correct.

Help welcome !

To my mind, it seems I can derive *:□⃞ from any environment and context because it is the axiomatic (sort) rule.

#maths #typetheory #lambdacalculus