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/