Readings shared March 23, 2025. https://jaalonso.github.io/vestigium/posts/2025/03/23-readings_shared_03-23-25 #Agda #Coq #FunctionalProgramming #HOL_Light #Haskell #ITP #IsabelleHOL #LeanProver #Math #Mizar #SetTheory

A review on mechanical proving and formalization of mathematical theorems. ~ Si Chen, Wensheng Yu, Guowei Dou, Qimeng Zhang. https://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=10930874 #ITP #Coq #IsabelleHOL #HOL_Light #Mizar #LeanProver #Math

Readings shared February 23, 2025. https://jaalonso.github.io/vestigium/posts/2025/02/23-readings_shared_02-23-25 #ATP #Coq #ITP #IsabelleHOL #Mace4 #Math #Mizar #Prover9 #Rocq

How to deepen your understanding of Mizar. ~ Alex Nelson. https://thmprover.wordpress.com/2025/02/22/how-to-deepen-your-understanding-of-mizar/ #ITP #Mizar

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/

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/

Readings shared January 4, 2025. https://jaalonso.github.io/vestigium/posts/2025/01/04-readings_shared_01-04-25 #ITP #IsabelleHOL #LeanProver #HOL_Light #Mizar #Math #Logic #Haskell #Python

Formalization of orthogonal complements of normed spaces. ~ Hiroyuki Okazaki. https://intapi.sciendo.com/pdf/10.2478/forma-2024-0010 #ITP #Mizar #Math

Universality of measure space. ~ Noboru Endou, Yasunari Shidama. https://intapi.sciendo.com/pdf/10.2478/forma-2024-0012 #ITP #Mizar #Math

Ascoli-Arzel`a theorem (Metric space version). ~ Keiichi Miyajima, Hiroshi Yamazaki. https://intapi.sciendo.com/pdf/10.2478/forma-2024-0011 #ITP #Mizar #Math

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/

Readings shared January 1, 2025. https://jaalonso.github.io/vestigium/posts/2025/01/01-readings_shared_01-01-25 #ITP #LeanProver #Lean4 #Mizar #Math #Haskell #Python

Formal proof of transcendence of the number e (Part II). ~ Yasushige Watase. https://intapi.sciendo.com/pdf/10.2478/forma-2024-0009 #ITP #Mizar #Math

Formal proof of transcendence of the number e (Part I). ~ Yasushige Watase. https://intapi.sciendo.com/pdf/10.2478/forma-2024-0008 #ITP #Mizar #Math

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/