After writing a POSIX-compliant shell script, then rewriting as a literate program using Noweb, I realize I might need to use an honest programming language like Standard ML to actually implement the desired program 😅

TIL ZSH is not a POSIX-compliant shell, after spending a couple hours trying to figure out why it doesn't accept my script the same way DASH, BASH, KSH, and other POSIX-compliant shells do...

Is there a way to estimate the number of top-level identifiers in an OCaml program?

Yeah, I'm not gonna lie, I am not a fan of the terminology used by Algebraic Geometers: their "immersions" aren't really what differential Geometers call "immersions" (instead AG's "unramified morphisms" are "immersions") 🫣

I just found Alexander Haberl, Tobias Nipkow, and Akihisa Yamada have formalized Greibech normal form in Isabelle/HOL a couple months ago. www.isa-afp.org/entries/Grei...

I was at a talk where the speaker used the symbol "※", which I've never seen before. Apparently it means the same thing as "N.B." en.wikipedia.org/wiki/Referen...

Read later: Turing's topological argument that [written] alphabets must be finite. divisbyzero.com/2010/05/27/t...

"The life of a human being is fleeting. The exhaled breath never waits for the inhaled one. Even dew before the wind is hardly a sufficient metaphor. It is the way of the world that whether one is wise or foolish, old or young, one never knows what will happen to one from one moment to the next."

I suppose my New Year's Resolution should be to blog more about Mizar. Writer's block comes so easily to me, though 😅

Getting bogged down proving stuff about associativity of matrix and scalar multiplication. What a way to start the new year...

I'm told (by some random website) that a book like Knuth's "The Art of Computer Programming" has an average of 250 words per page. If that's approximately correct, all 5 books have approximately 3904 pages or 976k words.

OK, this is funny. Someone started a Twitch channel with a computer program playing Pokemon. Each of the 10 keys on the device was mapped to digits 0, 1, 2, ..., 9; then the computer program calculated each digit of pi, and hit the corresponding key. Will pi win the game? arxiv.org/abs/2512.23143

If a context-free grammar is in Greibech normal form, then Earley parsing can be implemented using finitary methods (primitive recursive functions). But can we transform a context-free grammar into Greibech normal form using finitary methods (i.e., primitive recursive functions) alone?

I wish someone translated Weyl's "Theorie der Darstellung kontinuierlcher halb-einfacher Gruppen durch lineare Transformationen" papers into English, my German just isn't good enough :(

I have a friend trying to learn Mathematics (around an undergraduate level of understanding), and I wrote some notes to convey my "mental model" of Mathematics. It's somewhere between a wiki and a notebook. pqnelson.github.io/math/index.xml

I need some choice of notation for the Lagrange resolvent. Right now, I suppose `\rho` works fine enough, but it seems like there's gotta be some better choice...

Read later...

Gauss is overrated as a Mathematician, and we all know it.

Around this time of year, I remember when my grampa starting singing, "Frosty the snowman, had a very shiny nose..."

SKULL OF THOMAS AQUINAS: TAKE A LEFT NOW PRIEST: No, the GPS says we have to keep going— SKULL: I KNOW A SHORTCUT PRIEST: Do you remember the last ti— SKULL: FOR THOSE WITH FAITH, NO EVIDENCE IS NECESSARY; FOR THOSE WITHOUT IT, NO EVIDENCE WILL SUFFICE

[Narrator] They did, in fact, turn the Democratic Party into the Labour Party several years *earlier* thanks to the tireless work of David Short, Matt Yglesias, and friends.

You have a left Submodule, a right Submodule, and a...Bisubmodule? Subbimodule? Erm...

It seems bad to have two manifolds which are elementary equivalent as models of manifolds, but they are not homeomorphic... arxiv.org/abs/2512.05206

Typesetting complex numbers should look something like $x+\mathrm{i}y$ according to Springer's macros. For the quaternions, does that mean $t+\mathrm{i}x+\mathrm{j}y+\mathrm{k}z$ is the way to typeset a generic quaternion? 🤔

An alarming number of programmers either don't realize this is satire, or start making excuses for working for an evil corporation. www.mcsweeneys.net/articles/i-w...

Exercise: implement a proof checker for the Hilbert proof calculus from Bourbaki's foundations (a Hilbert epsilon calculus) using plain TeX as the implementation language.

It's amazing to me how much faster plain TeX is than LaTeX. I have a medium-sized project, producing 72 pages of output, run in a 1.074 seconds in plain TeX. LaTeX takes about 15 times longer on a comparably sized project. And plain TeX is *stable*.

Read later, this seems like a good "second or third book" on finite group theory after I Martin Isaacs's book and Aschbacher's book... arxiv.org/abs/2511.18392

I helped Dr Nipkow catch a few typos in his chapter on Red-Black trees (and elsewhere). In fact, I think this is the first book I am thanked in the preface 😇

Looking at Grothendieck's [Système de pseudo-droites]: notes manuscrites (1983-1984, s.d.). Cote no 154, 175 pages...and my goodness, that's terrible handwriting. Or is it just me? Does anyone find this legible? grothendieck.umontpellier.fr/archives-gro...

My god, some zealous grad students in the Lean community don't understand satisfiability is a predicate in the metalanguage, and results concerning soundness and completeness are metatheorems. "They're theorems!" ...not in the object logic, they're not...

I wonder how many of my readers recognize the allusion with the section title "Precedence lost and Precedence regained"...

I realized there are three audiences I'm writing for, but failing to actually communicate to each of them: (1) Mathematicians interested in *using* proof assistants (2) Mathematicians interested in *building* proof assistants (3) People interested in Foundations of Mathematics ...and maybe more?

Also, read later arxiv.org/abs/2511.10343

Read later arxiv.org/abs/2511.09553

Once you start thinking of AI as a war on humanity, on human thought, on human inquiry, on human labor, on nuance and critical thinking, it slots in pretty seamlessly with the right wing ideological project, oligarchical political projects, big tech's political projects, etc

Read later arxiv.org/abs/2511.03627

Don't forget: "Vielbein" refers to the frame field in *arbitrary* number of dimensions. "Vierbein" refers to the frame field specifically in *four* dimensions. ...because we couldn't use "frame field", that'd be crazy talk.

I just learned the inventor of Metamath, Norm McGill, passed away a few years ago, in 2021. I'm rather heartbroken to learn it.

"77.4.17 Remark: An optimistic note. The author's search for truth doesn’t amount to a hill of beans in this crazy world...

We can have a module over a (unital, associative) ring. Everyone knows this. But we can also have a module over a monad, or a Lie algebra, or a non-unital ring. What's the most general setting where we can define a module?

Random question: there's a cayote on campus which appears at random times. I've run across it (it's the size of a medium-small dog, or a little smaller than a wolf). Security says to call them if we see it...but what am I *supposed* to do with Cayotes? Play dead? Climb a tree? Don't move?

The Serre-Swan theorem strengthens the analogy "projective modules over rings are like vector bundles", prevalent in commutative algebra (and algebraic geometry). en.wikipedia.org/wiki/Serre%E...

I worked through one possible solution to proving Pelletier's problem 24 in the #Mizar #proofassistant, but there are others. thmprover.wordpress.com/2025/10/19/p...

There’s a free application, shutup10++, that lets you disable all the shitty windows stuff with a series of checkboxes. It even tracks if windows rolls anything back between updates and lets you reverse the changes with a click. I can personally recommend shutup10++ if you need to stick with windows

Every time I pick up my prescription, I swing by Burrito Express to pick up the Ross Perot Burrito. It's surprisingly good, for being named after a third party weirdo. en.wikipedia.org/wiki/Burrito...

Despite the tornados and thunder storms, I wrote a brief "worked example" of how to prove one of Pelletier's problems in the #Mizar #proofassistant. This is part of the "Mizar 101" series of posts. thmprover.wordpress.com/2025/10/14/s...

Uh, a tornado warning *and* a thunderstorm warming has just been issued for Los Angeles... I never lived through a "thunder tornado", but I don't think I want to...