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

Microsoft has been doing this stuff for literal decades, and only now programmers are concerned about quality. I feel like I've been shouting this from the rooftops for years, and now --- only *now* --- are people concerned. The horse has left the barn... techtrenches.substack.com/p/the-great-...

For the first time in months, it is raining. Quite heavily, too. Thank goodness I don't have to go to class today, I'd hate to run 5k in this weather, and wait for buses...

Read later, kinda interesting "dialect" of literate programming... arxiv.org/abs/2510.09073

I write a little fiction, nothing serious...because I realize there's a huge canon I have to work my way through, full of amazing writers like Jane Austen. I couldn't imagine a [fiction] writer admitting out loud to have not read Jane Austen, and not realizing they were missing out on it.

I'm not convinced Aschbacher's definition of a "building" generalizes Bourbaki's definition, but it's built on so many layers of abstraction it's hard to keep track of things 😂

I've started a "Mizar 101" series of posts oriented towards people who have just installed the #Mizar #proofassistant, but don't really know what to do from there. The first thing to check is that you installed Mizar correctly, that it "works". thmprover.wordpress.com/2025/10/11/h...

So I finished Gotrek & Felix Omnibus 4 wondering if Snorri ends up getting to the shrine of [dwarf god] and [event happening]. Then Omnibus 5 begins anachronistically between the first and second book. But...but...what happens to Snorri Nosebiter? Maybe I'll find out in Omnibus 6...

Read later arxiv.org/abs/2510.07851

OK, I was told my blog posts on Mizar are not simple enough for beginners, so I will start a "Mizar 101" series of blog posts which will work through even simpler material. ...I just need to think of even simpler material to write about...

TIL about the Lindamood Bell theory of reading, where the reader uses visualization to read each word instead of trying to pronounce each phoneme. Apparently, this helps a lot of people with dyslexia read stuff better (or, in some cases, at all).

What's the origin story of "preterms" and "pretypes" in type theory? I never got a clear history of the notions, and they seem pretty important even in simply typed lambda-calculus.

I just found out the paper I'm a co-author on, got posted to the arXiv yesterday. Neat.

Good grief, I am tired. I just returned home after visiting family for about a week. Tomorrow I need to get up at 5am, to catch a bus at 5:30am to take me to Caltech by 7am. Then I return home catching a bus at 3:45pm at Caltech, and I should get home around 4:45pm.

I'll be out of town visiting my grandparents for a week, so if you want to tell me my political opinions are stupid, you have until tomorrow...

The only work on "schemas" in logic seems to be Corcoran's "Schemata: the Concept of Schema in the History of Logic". Is there anything more substantial than the lip-service of "Schemes are formulas with metavariables"?

Yeah, I realize that TeX is a "sacred language" to me, and I am perfectly happy with that.

OCaml used to have a way to generate a standalone C program containing the bytecode interpreter...was this phased out or dropped?

Read later arxiv.org/abs/2305.15382

I wrote a little about "literate programming" used to implement proof assistants, mostly about the "literate programming". #LiterateProgramming #ProofAssistant #Logic #Mathematics thmprover.wordpress.com/2025/09/16/l...

I will be honest: I dislike open addressing in hash tables. It feels so poorly thought out... en.wikipedia.org/wiki/Open_ad...

TIL about "do-support", because my primary school never taught me grammar. en.wikipedia.org/wiki/Do-supp...

I have just finished the first pass at transcribing Mizar's parser into WEB. It consists of 1607 numbered paragraphs, spanning 544 pages. The index alone consists of 48 pages. There's still more I need to expand upon, specifically with parsing.

Is there some standard terminology for the components of set-builder notation? If I write {f(x) : x in A, phi[x]}, what do we call f(x) and phi[x]? The sample and constraint? What?

Scientists found evidence supporting Hawking's area law of entropy www.arxiv.org/abs/2509.08054

I just finished 161 chunks about the `extItem` class. Next up: 101 chunks about the `extSubexpression` class. Then the detour on parseraddition.pas will be done, and I can return to annotate Mizar's parser.

I like how the UML 2.5.1 standard offers a meta-diagram for each kind of diagram... www.omg.org/spec/UML/2.5...

I am just trying to focus on transcribing the details about Mizar's parser, I don't really want to comment on how shitty life is in the US and how mass shootings are a daily occurrence. I wonder if I could describe a "Mizar VM" similar to how Markarius did with his "Isar VM" in his PhD thesis...?