John D. Norton - Claims that information is fundamental are mistaken: The thermodynamic myth at the heart of information theory

See his article published in IAI News on 10th July 2026. "Considerations of information and computing complicate thermodynamic analysis and contribute precisely nothing." 

CEO and co-founder of Google DeepMind, Demis Hassabis, has recently speculated that information might be as fundamental as mass and energy. As AI hype rolls on, many like him are increasingly tempted to apply computing principles to reality as a whole. Those who support this view rely on the idea that information has a thermodynamic cost, as proposed by physicist Leo Szilard. 

See Happy Birthday Raymond Solomonoff (in particular 22:33 on how to get information from experiments) and Mike McCulloch on Why Everyone Should Care About Quantized Intertia.

I recently heard that the formalisation of the simplified Taylor/Wiles proof of Fermat's Last Theorem had been completed by Anthropic AI agents. I asked Google's AI how much energy this took and the estimate was of the order of one million MegaJoules which it says is equivalent to the annual power consumption of thirty US homes, so about the amount of electrical power I will have used in my lifetime.  What is the information content of the Lean proof? It was "13 million lines of Lean and proved 29,500 intermediate theorems" apparently it also proved some 800 or so other theorems which were not necessary for the proof of FLT, ... 

"The finished proof was checked by Lean; it uses just Lean’s three standard axioms, and a comparator confirmed that the theorem’s statement matches Mathlib’s own statement of FLT." What is a comparator?

"Comparator [apparently there is only one!] is a trustworthy judge for Lean proofs. It relies on having an existing Lean installation as well as:

  1. landrun, compiled from the main branch's source, present in PATH
  2. lean4export, at a version that is compatible with whatever Lean version your project is targeting, present in PATH    
  3. (optional) nanoda, compiled with a recent version of Rust. This is only necessary if you want to check with the nanoda kernel in addition to the builtin one. cargo build --release will place nanoda_bin in the target/release directory of the checked-out directory, this directory must be present in PATH."

Oh it's trustworthy, so that's OK then. I would hate to think that Million MegaJoules was all for nothing, ... 

See Fermat’s Last Theorem: The Curious Incident of the Boasting Frenchman and A “proof” of Fermat’s Last Theorem that fits the margin.

Comments

Post a Comment

Popular posts from this blog

Tensor Fields and Simplicial Complexes

Image
Listening to Freya Holmér last night I started to get glimmers of an idea I had long ago about how to represent vector spaces in computational processes using this recursive abstract type :  abstype 'a point = POINT   of {getx :  'a vector,       diff :  'a point -> 'a point,       move :  'a point -> 'a point,       scale : 'a -> 'a point,       proj :  'a point -> 'a} with    fun new i (op +) (op -) (op * ) dot =    let fun self x =  POINT       {getx = x,        move = fn (POINT pr) =>           (self (x + (#getx pr))),        diff = fn (POINT pr) =>          self (x - (#getx pr)),        scale = fn i =>          (self (x * i)),        proj = fn (POINT pr) =>     ...
Read more

FUTO FUBS

Image
I think this is the first time they've actually publicly announced anything about this project. See these posts: Eron Woolf on Why Open Source is Failing Matt Mikhailov and Vincent McKibbon on The Problem with Open Hardware Jason Kridner talking About BeagleBoard.org and Software Development .  See these places:  https://danielc.dev/rk/ https://github.com/petabyt/rk https://github.com/futo-org/ret See also  https://pine64.org/devices/pinebook_pro/ . Subscribe to  FUTO .  See  https://github.com/nir9/low-level-learning-resources/tree/master/setups/debian . Subscribe to  Nir Lichtman .  If you're looking for a cool init process, try  https://ctx.graphics/terminal/ . See  Artful Bytes - When to Use a RTOS  and  How to Create a Successful Open Source Project . 
Read more

Global Virtual Four Season School in The Foundations of Mathematics and Physics

Image
This is happening everywhere, all year around, just because of the nature of actual Human Knowledge. Invited speakers: a bunch of people who all know what they're talking about . On light and the nature of photographic process: Silver halide crystals only go off when exposed to light at certain frequencies, so the crystals have to be embedded in a glycerine matrix with layers of dye to make the film respond to visible light. Subscribe to  Smarter Every Day 2 . See  Joel Hamkins interviewed on About Logic .
Read more