Posts

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