Lmst

I wrote a brief post about redefinitions in Mizar.

Redefinitions occur when we specialize the parameters of a definition, and it simplifies the "right-hand side" of the definition to something far simpler (or more useful).

Redefinitions also allow us to tack on properties like "commutative" or "idempotent" to definitions, so Mizar can automatically use them when reasoning about the terms.

#Mizar #ProofAssistant #definition #redefinition #mathematics

https://thmprover.wordpress.com/2025/06/24/redefinitions-in-mizar/

For HOL, the axiom of infinity (and I guess Hilbert's operator) gives it its strength. Can we replace it with a weaker alternative? Can we get something as weak as, say, PRA?

#ProofAssistant #HOL #mathematics

Change my mind: pseudogroups are the "wrong way" to formalize differential geometry.

What's wrong with formalizing charts and atlases, then a manifold is a set equipped with a maximal atlas?

We could formalize, e.g., complex manifolds using G-structures.

What is wrong with this approach?

#Mathematics #proofassistant #differentialgeometry

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?

#ProofAssistant #Book #ComputerScience

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/

#Mizar #proofassistant #mathematics

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{Set}\) in Mizar, I'd suggest using \(\mathbf{G}(\omega)\) as the collection of objects underlying it (making it, effectively, the category \(\mathbf{ZFSet}\)).

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