The Eternal Doorman

He's very polite: because some of these responses he got from ChatGPT are hilarious. The main observation seems to be that AIs don't do well with maths because of the way most published mathematical literature is written, as students know only too well, is missing most of the dynamical elements in the proof process and is presented entirely in terms of truth-functional statements.  Imre Lakatos described the process at length in his book Proofs and Refutations . During the development of the subject now called Additive combinatorics certain definitions such sumset were made, and because these somewhat arbitrary definitions turned out to be fruitful in some way, they became widely used and thereby imposed a certain structure on the development of the field. But those definitions were not a priori necessary, yet they now have a central rôle in the subject as it was developed. So, having thus defined the field, the process of proving theorems becomes heavily constrained by thes...

I wonder if it's possible to siphon the water over the landfall? You would need just enough flow to match the river, and then a little more to drain the lake. This company have made a siphon with a capacity of over 23,050 m³ per hour with a height difference of approximately 1.2 meters. See  VAN HECK’S LARGEST SIPHON SYSTEM IN OBERHAUSEN . A critical issue with a siphon is the height of the obstruction, which can be at most 10m so maybe you'd have to bury the tube: It's amazing how little engineering research seems to have been done on the use of siphons. Subscribe to Atlas Copco Vacuum Solutions . Stuart Lane, Professor of Geomorphology at University of Lausanne 'You can't engineer yourself out of something of this magnitude' Subscribe to France24 . See  Looks Like Blatten is Gone Now, ... Another update this morning: Another update the next morning (31 May)   And another update: the river has started to flow again and the water level above the debris cone has...

Illustration from Project Gutenberg's The Tenniel Illustrations for Carroll's Alice in Wonderland by Sir John Tenniel. Thinking about the linux desktop audio problem: I'm not the only one who finds this weird: https://t.co/b2BZMiak07 — eternal Doorman (@IanANGrant66) May 17, 2025  I noticed that if you change the volume using the Gnome volume keys it changes it in jumps. Usually you don't notice, but if you play a pure sine tone then you can easily hear the distortion. If you want to play with pipewire from C on Ubuntu 24.04 then it's really easy. The pipewire tutorials and examples can be compiled and run if you just first install the pipewire-0.3-dev package with sudo apt install libpipewire-0.3-dev But the API is sooo far away from pluggable, typed streams that I find it quite depressing. Is it because nobody understands the necessary type system . See  Programming Channel Processes and Alice's Adventures In The Wonderland Wide Web . [Update: y...

This is interesting. These algorithms can be used to program silicon as well as general purpose machines. The hardest part seems to be parsing the tensor files! See  https://github.com/LaurieWired/MatrixMultiplicationOptimization  and  https://github.com/mkauers/matrix-multiplication  and the papers  Flip Graphs With Symmetry and New Matrix Multiplication Schemes  and  Consequences of the Moosbauer-Poole Algorithms . I wonder if people will start using techniques like this to devise algorithms customised to multiplication of particular kinds of matrices. See  Scott Aaronson - Why Philosophers Should Care About Computational Complexity . Subscribe to Laurie Wired .

... all with Eben Upton's signature, forged! Subscribe to Jeff Geerling .

You don't have to soak the peanut butter jar if you eat all the peanut butter first, ...  Subscribe to Julie Nolke .

This follows nicely from Jenann Ismael's talk  Jenann Ismael - Laplace meets Godel: How Self reference Foils Prediction  and also Edward Frenkel's talk Norman Wildberger and Dean Rubine Rewriting History and Edward Frenkel Offering Free Psychoanalysis . 32:33 There's an interesting observation about the Ackermann function  and addition, multiplication and exponentiation here. See Philip Wadler's talk "Categories for the Working Hacker" in  Philip Wadler - Propositions as Types . 46:11 Interesting thing about over-parametrised LLMs. 51:17 on MP*=RE see  https://pirsa.org/20050011  and this mathoverflow discussion  MIP*=RE theorem and its impact on logic and proof theory . 1:06:41 Interesting thing about non-linearity in quantum mechanics which I'd never heard of before. See Daniel S. Abrams and Seth Lloyd's  Nonlinear quantum mechanics implies polynomial-time solution for NP-complete and #P problems   (1998). 1:18:55 On quantum computin...

  There is a generalised form of the Catalan numbers which sheds some light on series solutions to polynomials. It turns out that this more general series was discovered  by a Mongolian mathematician a century before Catalan described the Catalan series. See  Numberphile - Sophie Maclean on the Catalan Numbers  and also  Terence Tao - Using Claude, ChatGPT to Formalise A Theorem About Magmas in Lean and More Robotics with Terence Tao . See N. J. Wildberger and Dean Rubine  A Hyper-Catalan Series Solution to Polynomial Equations, and the Geode  in The American Mathematical Monthly. Subscribe to Insights into Mathematics .  Subscribe to Simons Centre for Geometry and Physics . Here's the video he mentions: So that's why it's important to read Toby's book:  Toby's 3D model of a "Four-dimensional Penrose Triangle" .   Subscribe to Edward Frenkel . 

This is great. Especially when she finds Peter The Great in Deptford, and the ride on the DLR at the end. Subscribe to Imalittlemole .

See  Physical Geography Animated in Switzerland .     This was ealier today: Subscribe to Blick .  Not completely, but now there will be a lake there,... Subscribe to Unwetter ChaseR .  Here's Silki's video from earlier today: I guess this is the end of the season for the Hotel Fafleralp up the valley too:   Subscribe to On The Pulse with Silki . And last night TheGeoModels did a video about it: Subscribe to TheGeoModels .

This is how AI is going to destroy the world: businesses are going to lay-off employees and their tech is going to go to hell because there'll be nobody in the office who can see what a mess the AI is making of everything until it's too late. But that won't happen before they've bought 3KW power supplies for the machines that are running the AI. See also  Defensive Security And Level1 Techs on Brokenness Everywhere . Subscribe to Level1 Techs .

There's this place, ... I know it well.   Really amazing graphic effects you can do with Unicode accents! It's all my fault. She's turned herself into one component in a huge global modular synth. See  Emily Hopkins Reinventing The Harp . Subscribe to Harp Lady .  And Moritz Klein has this Eurorack module component which just has a breadboard on it so you can plug just about anything into a modular synth rack now, maybe including a harpist or two, ... or a 6502 ... 13:33  This is the gnome desktop volume keys problem, but there you can fix it just by slowly ramping up the volume with a "lerp" see  Using Pipewire to Make A Music Synthesizer . Erica Synths sell a kit for this, see  https://www.ericasynths.lv/shop/diy-kits-1/edu-diy-fm-drum/  and you can get Moritz's LABOR breadboard module from them too:  https://www.ericasynths.lv/shop/diy-kits-1/edu-diy-labor/ . Subscribe to  Moritz Klein . Pile - Born at Night From  Sunshine and Balanc...

Wow, that is a lot of broken amplifiers! People should look after their stuff better! Get your amp fixed, and/or buy her Scorpion Pilot Light Jewels for Fender-style Amps here . Subscribe to Fazio Electric .

Subscribe to Defensive Security Podcast . Subscribe to Level1Techs . 

  What a great co-author! See  Jenann Ismael - Laplace meets Godel: How Self reference Foils Prediction . Subscribe to Laura Pausini TV . Tom Waits - Heart Attack & Vine (Screamin' Jay Hawkins cover) Subscribe to Screemin' Jay Hawkins . It started out so hopeful! What went wrong, Donald?  Subscribe to Laura Pausini .

... and an update ( 11:00 ) about the IM Athena lander failure, ... the optical guidance system had problems dealing with with long shadows. See these posts . Subscribe to Scott Manley .

Here he is using Lean in the VS Code IDE with GitHub copilot to formally prove a part of the Polynomial Freiman-Ruzsa Conjecture extension blueprint, but the GitHub copilot LLM isn't trained on anything outside Mathlib ( 14:39 ), so it can't help with the PFR extensions they will be putting in to Mathlib when the project is finished. He's doing this on his laptop, so the compiler gets a bit slow since the proof is several thousand lines long now. At 16:13 about sometimes not needing certain hypotheses when proving lemmas. I guess that's because those lemmas are really more general than just this theory, and that's the sort of thing that Category Theory shows: some things are true in a category of which this theory is just is one particular instance. See Terence Tao - Using Claude, ChatGPT to Formalise A Theorem About Magmas in Lean . I think this sheds some light on the proof of the Deduction Theorem in Church's paper "A Formulation of the Simple Theory...

The theorem is that x=(yx)((xz)z) implies the singleton law x=y . I guess this is from the Equational Theories Project : The purpose of this project, launched on Sep 25, 2024, is to explore the space of equational theories of magmas , ordered by implication. To begin with we shall focus only on theories of a single equation, and specifically on the 4,694 equational laws involving at most four magma operations, up to symmetry and relabelling (here is the list in Lean and in plain text ). This creates 4694*(4694-1) = 22,028,942 implications that need to be proven or disproven, creating both “implications” and “anti-implications”. The singleton law : This is the strongest law, satisfied only by the trivial magmas: the singleton and empty magmas. Many laws are equivalent to this law; informally, they are so "overdetermined" that they can only be satisfied by trivial magmas. In fact, from our list of 4694 laws, exactly 1495 other laws are equivalent to this one. The equations w...

Permafrost in the mountains is melting and the consequences are very dramatic: rocks shooting out like bullets. This is above the village of Blatten which has been evacuated. This isn't the only Swiss village under threat. 14:02 Andreas Speiss ( @AndreasSpeiss ) should be able to help with data collection, or he could if it wasn't illegal: see 465 Rutgers University Confirmed: Meshtastic and LoRa are dangerous . Her video from yesterday: Here's a warning about the potential eruption in Pozzuoli in Naples where they do have a comprehensive network of sensors, and it's telling them things they don't want to hear! Buy her a coffee and subscribe to On The Pulse with Silki .

This is really excellent: See also  A Participatory Universe in the Realist Mode: On the Separation of Observational and Agentive Perspectives in Classical and Quantum Mechanics . Here is something I wrote in 2012 that gives an explicit example with some formulae: I feel really left-out because nobody I know sent me this XKCD drawing. You can actually compute that as accurately as you like, can't you?: I guess I don't spend enough time on social media, ...  So this has real practical consequences and tells us something about how we should think about these kinds of systems. We need to be able to design convergent processes which have stable fixpoints, like the XKCD drawing. See Gabriele Carcassi on Physical Convergence and Richard's paradox . And on how we construct and test machines, see Julia Galef on Aumann's Agreement Theorem and Robert J. Aumann's very short 1976 paper Agreeing to Disagree . Subscribe to Santa Fe Institute .

It goes to Austin, San Antonio, El Paso and a bunch of other places. Subscribe to Goldilocks Walks .

Subscribe to Crime Pays but Botany Doesn't .

Subscribe to Al Jazeera English .  Seems like it's just the good old free market: here's a Middle East Eye report on the gold smuggling and laundering through the UAE. See also Livelihoods, Power, and Choice: The Vulnerability of the Northern Rizaygat of Darfur, Sudan and Ghana river pollution: Illegal gold mining contaminating drinking water . Subscribe to Middle East Eye .  Krishnan Guru-Murthi did a report on Channel-4 a few months ago. See Krishnan Guru-Murthi in South Kordofan : Subscribe to Unreported World .  One way to look at it is the fake economics of a dying empire taking millions of people who never knew any of that wealth down with it. See  Film - Surviving Progress (2011) . 

He diligently posts at least two short talks on his YouTube channel every Saturday, and occasionally he re-enacts lectures he has given to a real audience, rather than a virtual audience on YouTube. This is one such re-enacted lecture on the Poincaré conjecture , Quantum Knot Invariants and the Jones Polynomial .  It's really excellent. Knot theory is now very clearly a part of polymer chemistry, and, when you think about that, it's really a very interesting thing. It means that the properties of organic chemical compounds like long-chain polymers are simply not reducible to the properties of their constituent atoms . Full stop! See the paper Big data comparison of quantum invariants by Daniel Tubbenhauer and Victor Zhang and the online database Knot Invariant Comparison by Zhang. Also ( 54:17 ) the Dioscuri Center in Topological Data Analysis site https://dioscuri-tda.org/BallMapperKnots.html . These data are only up to about 15 crossings. So how much do we know now abou...

This is about how Verizon and CISCO together caused a huge Internet outage on August 12, 2014 . Six days after I posted this: A Funny way to Earn a Living . It's good: they get an old CISCO 6500 and set it up and fill the router FIB table content-addressable memory to show what happens. Subscribe to The Serial Port .

This is a beautifully made film. I was released on September 11, 2011 and six days later the Occupy Wall Street protests began. Directors : Mathieu Roy, Harold Crooks Cast: Ronald Wright, Mark Levine, Robert Wright, Jane Goodall, Marina Silva Produced by Martin Scorcese Another gift stolen from Canada. See https://www.nfb.ca/film/surviving-progress/ . Subscribe to Best Documentary .

The automatic weather reporting equipment and the runway alignment indicator lights were not working at the airstrip at the time of the crash. And the advisories of this are crazily abbreviated, apparently because the system used to work over 300 baud teletype.  Here's the original video of two days ago:  Subscribe to Blancolirio .

Subscribe to Eleanor Morton .

There are two papers to be presented here that caught my attention: Dependent Directed Wiring Diagrams for Composing Instantaneous Systems by Keri D’Angelo and Sophie Libkind. See Using Pipewire to Make A Music Synthesizer . Actegories and Copowers with Applications to Message Passing Semantics by Robin Cockett and Melika Norouzbeygi. (See Categorical Semantics of Higher-Order Message Passing for the background and Compiler Coffee Club - Interning Cyclic Types in a Compiler ). See the conference web site https://gataslab.org/act2025/act2025 .

It tanked. "Ethan, as a character, feels like an afterthought in his own movie". Yeah, tell me about it! Subscribe to Deepfocuslens . And speaking of movies,..  This remake of I, Robot is heading the same way, see  Hitachi HD44780U LCD Display Fonts :  Subscribe to Computerphile .  But, ... not everyone agrees! See the spoiler-free Letterbox review that will make your CPU start heating up at  https://letterboxd.com/ManCarrying/ . Subscribe to Woman Carrying Man . So, AI threatens to end world by doing hilarious impression of Donald J. Trump See the paper:  https://arxiv.org/abs/2502.15840 . Subscribe to ThoJoe .

See  https://github.com/SeaOfNodes/Simple and https://github.com/cliffclick/aa . This example at the beginning of type-checking a parser record structure is reminiscent of the problem of typing/sorting higher-order polyadic π-calculus . See Using Pipewire to Make A Music Synthesizer . I think there is some maths by Grothendeick that should help, see Category of elements in Wikipedia and Grothendieck construction in nLab . There is a use-case in David MacQueen's model of  types of higher-order functors: see David Macqueen's A Semantics for Higher-order Functors (1997) and Higher-order modules and the phase distinction by Harper, Mitchell and Moggi : The hard part is probably deciding on what is the most useful phase distinction to introduce. Subscribe to Cliff Click .

In the US the plumbing and HVAC industry is worth almost as much as the software industry. And they're getting ripped off for advertising!  Subscribe to Morning Brew .

When they start developing the encrypted backup solution I hope they take into account that people need encrypted distributed backups for more than just the photos in their photo sharing server. I would also like to know more about how they manage sharing of content. That again is something that is a very general project. I wrote that before I heard the bit at 27:32 about federated cross-instance albums and sharing. Two days ago FUTO gave a microgrant to Peergos and mentioned that they'e working on an Immich plugin. 3:45 "Leave a comment or send us an email". I'd prefer to send tem an email, but I can't find their email address. It's not on their YT channel page , nor is it on their web site , AFAICS. About software distribution and maintenance: see René Rebe Hacking on Twitch to Earn A Living . Subscribe to FUTO .

He's written a compiler and is going to write a text editor for Wayland,... The problem is that the Linux development tools have become unmanageable for distribution maintainers. This was from eight month's ago: I thought FUTO ought to be interested in T2sde. See  Nir Lichtman's 12-minute Linux Distribution Video  and  Eron Woolf on Why Open Source is Failing  and for the bigger picture:  Using Pipewire to Make A Music Synthesizer .  I hope this doesn't cause him to get SWATted again:  Hacking Linux in the Federal Republic of Germany? Mein Gott! Subscribe to  Code Therapy w/René Rebe .

Subscribe to Julie Nolke . Actually this one's from Switzerland, originally, but sent via Canada: Subscribe to Academy of Ideas .

... played on a theorbo. He has a playlist of Jimi Hendrix songs and another of various classical pieces on baroque guitar and theorbo .  Subscribe to Stefano Maiorana .

This is a nice counterpoint to Google's ridiculous nonsense the other day. See the full article: Philosophy Eats AI . You'll have to pay to do that, but it's only for rich people. Here's their playlist of review article reviews . Subscribe to MIT Sloane Management Review .

  Subscribe to AuswaertigesAmtDE .

Made in New Zealand by Sam Gill . Subscribe to Dust .

... here's some truth: Subscribe to Fireship .

The talking book: See her latest video which is part 2 of a collaboration with Simone Giertz: Subscribe to Dina.A.Amin . Subscribe to Simone Giertz .

Here's a review of a high-end Chinese Memblaze SSD 3 - 7 TB, 14GB/s Read, 10GB/s Write, US$940 in quantities of 10 or more. Good for hosting IPFS nodes too, I shouldn't wonder: Apparently those are just baby SSDs: So what about all these governments around the world that aren't capable of keeping a record of who their citizens are/were? "Oh, we didn't manage to keep a proper record of your citizenship, but here's a photocopy of an index card we made with your name and the number of the certificate we issued, hand-written in pencil by who knows who?" That's the UK Government, let's talk about South Africa, Zimbabwe and Bolivia later, ... Subscribe to Level1 Techs .

This looks interesting. See the article here https://assumptionsofphysics.org/essays/2025-05-15-convergence . Reading that I realised that Claude AI is presumably named after Claude Shannon who wrote a Bell Labs Technical report with the title "A Mathematical Theory of Communication" . In it he proves the source coding theorem : In information theory, Shannon's source coding theorem (or noiseless coding theorem) establishes the statistical limits to possible data compression for data whose source is an independent identically-distributed random variable, and the operational meaning of the Shannon entropy . Following Ernst Mach , one might think of any physical laboratory apparatus as a device for producing streams of symbols; then a physical theory is a formal mechanism for reproducing any experimentally observed sequence resulting from the input of parameters characterising the particular experimental setup:     "The goal which it (physical science) has set itself ...

This is riveting! He talks about the early counterculture at Berkeley, IBM punched cards and the University of California administration they ruled and the bulletin board system they put together with Douglas Engelbart's old SDS-940 mainframe, ... see also https://computerhistory.org/profile/lee-felsenstein/ . Subscribe to Sayaka's Digital Attic . Here's a short documentary-style video: Subscribe to  Galliot . Lee Felsenstein's book Me and My Big Ideas is only available on Amazon , as far as I can see. Apple books lists it , but gives no way to actually buy it! Booksellers interested in stocking it can contact IngramSpark who list Waterstones and Foyles amongst their UK resellers. It's hard to find anything about his new Community Memory project on Google search. For more on Jerri Ellsworth see Thinking About How AI Can Make Better Programmers, ... and for more on AI and truth, see Gabriele Carcassi on Physical Convergence .

I finally got the bit-mapped fonts from the Hitachi "1602" display :  Here's some JavaScript: const HD44780U01ASCII=[ [],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[], [],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ], [4, 4, 4, 4, 0, 0, 4, 0, 0, 0, ], [10, 10, 10, 0, 0, 0, 0, 0, 0, 0, ], [10, 10, 31, 10, 31, 10, 10, 0, 0, 0, ], [4, 15, 20, 14, 5, 30, 4, 0, 0, 0, ], [24, 25, 2, 4, 8, 19, 3, 0, 0, 0, ], [12, 18, 20, 8, 21, 18, 13, 0, 0, 0, ], [12, 4, 8, 0, 0, 0, 0, 0, 0, 0, ], [2, 4, 8, 8, 8, 4, 2, 0, 0, 0, ], [8, 4, 2, 2, 2, 4, 8, 0, 0, 0, ], [0, 4, 21, 14, 21, 4, 0, 0, 0, 0, ], [0, 4, 4, 31, 4, 4, 0, 0, 0, 0, ], [0, 0, 0, 0, 12, 4, 8, 0, 0, 0, ], [0, 0, 0, 31, 0, 0, 0, 0, 0, 0, ], [0, 0, 0, 0, 0, 12, 12, 0, 0, 0, ], [0, 1, 2, 4, 8, 16, 0, 0, 0, 0, ], [14, 17, 19, 21, 25, 17, 14, 0, 0, 0, ], [4, 12, 4, 4, 4, 4, 14, 0, 0, 0, ], [14, 17, 1, 2, 4, 8, 31, 0, 0, 0, ], [31, 2, 4, 2, 1, 17, 14, 0, 0, 0, ], [2, 6, 10, 18, 31, 2, 2, 0, 0,...