I am in the middle of formalizing Matrix Groups in Mizar, and I ran into a surprising error...so I wrote a blog post about fixing it and how to avoid it in the future.

The problem was a typing error, something which us humans would identify "They're the same thing" but a computer panics about.

#Mizar #proofassistant

https://thmprover.wordpress.com/2025/04/28/debugging-a-105-error/

I wrote a bit about how to get a better understanding at what Mizar is "doing under the hood".

The short answer is to develop a mental model (an informal abstract machine) by studying formalizations, and trying to formalize stuff with this mental model.

After all, how do you learn to do something without actually doing it? It helps to see "what's going on" when you write, e.g., a definition, but it "just" generates some new constants (possibly requiring proofs that they're well-defined).

#Mizar #ProofAssistant #Mathematics

https://thmprover.wordpress.com/2025/02/22/how-to-deepen-your-understanding-of-mizar/

What are some good books to get someone interested in proof assistants? I'm curious what you guys recommend.

My cousin is getting interested in proof assistants. He already has John Harrison's "Handbook of Practical Logic and Automated Reasoning".

What else would you guys recommend?

I've been thinking about this for a while, sketching out the formalization of the tensor product in Mizar.

It's kind of long, not as step-by-step oriented as previous projects, because I wanted to give a better sense of "What it's like to formalize something". You don't have someone giving you step-by-step milestones, you have to figure it out on your own!

At the same time, even granting all of that, I gave a lot of suggested milestones (albeit informally and without fanfare).

#Mizar #ProofAssistant #TensorProduct #Tensor #Mathematics

https://thmprover.wordpress.com/2025/01/17/tensor-products-in-mizar/

Another project idea: formalize the semantics of HOL in Mizar.

This is actually quite straightforward, since Andrew Pitts formalized most of the work back in his 1991 presentation of HOL's semantics.

But I don't think it's been formalized! Perhaps it has, I don't know, I wrote this up as the city I live is engulfed in flames: I didn't have the luxury of time to find out.

But that shouldn't stop you from having fun! There are a million variations to consider, as well: typeclasses, inductive types, etc. etc. etc.

#Mizar #HOL #ProofAssistant #Semantics

https://thmprover.wordpress.com/2025/01/14/hol-in-mizar/

Project idea: formalize error correcting codes in Mizar.

Error-correcting codes are a beautiful subject, mostly because they're linear algebra over finite fields (and linear algebra is beautiful).

But there are exceptional connections in the subject: the Golay code and the Leech lattice especially connect with disparate subjects.

To give one sense of connection, I gave Robert A Wilson's construction of the Leech lattice using the octonions as a "milestone".

#Mizar #ProofAssistant #ErrorCorrectingCodes #LeechLattice #LinearAlgebra #Octonions #GolayCode

https://thmprover.wordpress.com/2025/01/09/from-error-correcting-codes-to-the-leech-lattice/

I reviewed how Mizar formalizes the Polynomial ring (and, really, how it formalizes polynomials).

There's quite a bit to it, but every proof assistant appears to use the same strategy: it's basically the monoid algebra for the free monoid generated by monomials over the indeterminates.

#Mizar #ProofAssistant #Polynomial

https://thmprover.wordpress.com/2025/01/07/ring-of-polynomials-in-mizar/

Another Thursday project idea for formalizing stuff in Mizar: The Icosians!

The Icosian group is isomorphic to the binary icosahedral group, but built out of quaternions.

We can use them to form a ring, also (confusingly) called the Icosians.

You can then form a lattice out of them, and it's isomorphic to the root lattice for the E8. It's really quite amazingly beautiful!

#Mizar #Quaternions #Icosians #ProofAssistant #E8 #Lattice

https://thmprover.wordpress.com/2025/01/02/icosians-in-mizar/

I (started) a review of the formalization of category theory in Mizar.

There are three separate ways to formalize a "category" in mathematics, and Mizar faithfully formalizes each different version.

#Mizar #ProofAssistant

https://thmprover.wordpress.com/2024/12/30/review-category-theory-in-mml-part-1/

Another project idea: formalize the universal property of products for sets in Mizar.

I did this for the product group, and it was a lot of fun. Plus, I learned a thing or two about products of an _infinite_ family of groups.

This work would underlie formalizing the universal property for the direct property of 1-sorted objects and later for modules over rings (and vector spaces over fields). So it's a critical "first step" towards greater things!

https://thmprover.wordpress.com/2024/12/26/universal-properties-for-sets/

I wrote a brief review of universes in Mizar.

Mizar has an axiom that for any set, there exists a *Tarski* universe containing it.

However, this is not necessarily the same as a *Grothendieck* universe.

It turns out, when we take a transitive set $X$ and look for the smallest Tarski universe containing it $X\in \mathbf{T}(X)$ and the smallest Grothendieck universe containing it $X\in \mathbf{G}(X)$, the two coincide $\mathbf{T}(X)=\mathbf{G}(X)$.

In general, though, we have $\mathbf{T}(X)\subseteq \mathbf{G}(X)$.

What's more interesting is that we can form the smallest Grothendieck universe containing the natural numbers $\mathbf{G}(\omega )$ and this is a model for ZF(C). Roland Coghetto wrote a couple recent articles proving all our favorite sets live in it. If you were to formalize the category $\mathbf{S}\mathbf{e}\mathbf{t}$ in Mizar, I'd suggest using $\mathbf{G}(\omega )$ as the collection of objects underlying it (making it, effectively, the category $\mathbf{Z}\mathbf{F}\mathbf{S}\mathbf{e}\mathbf{t}$).

#Mizar #proofassistant #logic #universe #mathematics

https://thmprover.wordpress.com/2024/12/23/universes-in-mizar/

Want to formalize something in Mizar?

Formalize the Octonions!

I have sketched out what this would look like, and relate it to pre-existing formalizations in Mizar.

#Mizar #proofassistant #mathematics #octonion

https://thmprover.wordpress.com/2024/12/19/formalize-the-octonions/

Want to formalize something in Mizar but don't know where to begin?

I'm starting a new series of posts with project ideas, starting with Loops! They're needed to formalize the sporadic groups (as found in, e.g., Aschbacher's book "Sporadic Groups").

#Mizar #proofassistant #mathematics #grouptheory

https://thmprover.wordpress.com/2024/12/16/loops-in-mizar/

I have been formalizing finite group theory in Mizar, and I am about to formalize representation theory.

So I thought I would write some "notes to myself" about it.

#proofassistant #grouptheory #RepresentationTheory #Mizar

https://thmprover.wordpress.com/2024/12/13/plans-for-representation-theory-in-mizar/

Announcement: formalizing Homology Groups in Mizar.

My friend, Sebastian Koch, is formalizing homology groups in Mizar and he's looking for collaborators.

If you're interested in formalizing something in Mizar, or if you're interested in homology groups, then this is a good opportunity to do something!

#Mizar #proofassistant #homology #algebaictopology #topology

https://thmprover.wordpress.com/2024/11/11/announcement-formalizing-homology-groups-in-mizar/

I have written a bit more about formalizing cosets of groups in Mizar.

Like other posts in my review of Group Theory in Mizar, this "walks through the thought process" underlying formalization of Mathematics.

#Mizar #GroupTheory #Math #proof #ProofAssistant

https://thmprover.wordpress.com/2024/10/28/cosets-of-groups-in-mizar/

What is a "structure" in Mizar?

This was always one of the most confusing things to me when I first got started with #Mizar since the answer requires a little bit of Model Theory, which isn't adequately taught in the US to "generic Mathematicians".

The answer is surprisingly deep yet simple: it's "just" a finite partial map in the Metatheory. This can be made precise using something like #Isabelle as the Metatheory (as done in the Isabelle/Mizar project).

We can also use a finite set of "attribute"-value pairs, which is called "first-class aggregates" (or "first-class structures") since they're defined like any other notion in Mizar, without special metatheoretic considerations. And they're useful for doing graph theory!

#Mizar #ProofAssistant #ModelTheory #Model_Theory #Logic #Mathematics

https://thmprover.wordpress.com/2024/10/04/what-is-a-structure-in-mizar/

One thing that has piqued my interest is something based off of Hilbert's programme, applicable to proof assistants.

Suppose I write a proof assistant in Standard ML. Then I use it to prove some function can be added to the kernel without jeopardizing the soundness of the system. I would like to dynamically extend the running program by compiling this function, and adding it to the program.

Hilbert's programme had something like this (as I understand it, they called it the epsilon substitution method) whereby a theorem stated in "idealized mathematics" which states and proves a claim about "finitary mathematics" can be "imported" back into the finitary metatheory, even if the finitary metatheory cannot prove it directly.

I think John Harrison called such a scheme as I've outlined "computational reflection".

It'd be neat to see a toy model of it.