Frankly speaking ...

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. This article follows that idea from first principles to wider systems. It moves from Shannon’s formal definition of information, through biology and thermodynamics, then into active theoretical debates in physics...

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...

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...