Posts

Information Theory as the Fundamental Architecture of Reality

Image
Introduction: The Informational Universe We typically perceive our world through the lens of tangible matter and flowing energy. We see a landscape of atoms, forces, and heat. However, modern science is beginning to realise that these physical properties might merely be the surface of a deeper architecture. At its most fundamental level, the universe appears to be composed of “bits” of information. Consider the extraordinary feat of a single microscopic cell: how does it “know” how to construct a complex human being? The answer lies not just in chemistry but in the sophisticated processing of data. By shifting our perspective to information theory, we can begin to decode the underlying software of existence and see ourselves as nodes within a vast, self-optimising system. Information Theory: Claude Shannon and the Mathematics of Meaning Before any of this can make sense, it helps to ask a deceptively simple question: what actually counts as “information”? In his 1948 paper A Ma...
Post a Comment
Read more

Is Gravity Just Spacetime's Temperature?

Image
Why This Debate Matters Contemporary physics faces a quiet but profound crisis. Our picture of the universe rests on two extraordinary frameworks that do not fit neatly together: General Relativity (GR), which describes spacetime as a smooth continuum curved by mass, and Quantum Mechanics (QM), which describes reality as discrete particles governed by chance. That tension sits alongside another stubborn cosmic puzzle: if the second law of thermodynamics dictates that the universe must become increasingly disordered over time, how can an expanding cosmos give rise to complex, ordered structures like galaxies, stars, planets, and life? Standard cosmology often attributes cosmic acceleration to a static cosmological constant or an undetected form of dynamical dark energy. Gravity from Entropy (GfE), developed by mathematician Ginestra Bianconi , offers a fresh perspective. Rather than adding missing particles or modifying GR arbitrarily, GfE treats gravity as an emergent, thermo...
1 comment
Read more

Using Lean 4 for Mathematics Proofs

Image
Using Lean 4 for Mathematics Proofs In the previous post, I explored Lean 4 as a functional programming language. If you already know functional languages like Haskell, you will recognise a lot of familiar ideas. Where Lean starts to feel different is in its annotations and, especially, in its use of tactics with dependent types. To make that concrete, I will walk through a small mathematical proof in Lean 4. The goal is to show an irrationality result. The classic classroom example is that  2 – √  is irrational, but that proof needs extra machinery. Here, I will use a simpler example that only needs basic arithmetic. I will start with the maths proof, then translate the same idea into Lean 4. I like this proof because it is compact. It is the classic “one side must be even, the other must be odd” contradiction. Mathematics: Prove that  log 2 ( 3 )  is irrational I start by assuming  log 2 ( 3 )  is rational. That means there exist positive integers...
1 comment
Read more