Mizar: The first usable proof assistant for mathematics

Mizar는 폴란드 비아위스토크 대학의 Andrzej Trybulec가 개발한 최초의 실용적인 수학 증명 보조 도구로, 자연스러운 수학적 언어를 포착하는 데 중점을 두었다. 냉전 시기 동서 진영의 분단으로 인해 서방에서는 오랫동안 주목받지 못했으나, 1993년 QED 선언 이후 그 중요성이 재조명되었다. Mizar는 강력한 집합론 기반과 자연스러운 속성 시스템을 갖추었으며, 오늘날 증명 보조 도구들의 증명 언어와 수학 라이브러리 구축에 큰 영향을 미쳤다. 2023년에는 Mizar 50주년을 맞아 ITP 학회가 비아위스토크에서 개최되었다.

https://lawrencecpaulson.github.io//2026/05/07/Mizar.html

#proofassistant #formalverification #mathematics #mizar #theoremproving

**Theorem proving with the real numbers**
https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-408.html
by John Robert Harrison
November 1996

The author used #HOL to formalise real numbers, including metric, sequences and limits, continuity and differentiation, power series and transcendental functions, integration.

There is also a #CAS and IEEE floating standard verification tools.

#ProofAssistant #Math #FormalVerification #Logic #PLT

50 years of proof assistants
https://lawrencecpaulson.github.io//2025/12/05/History_of_Proof_Assistants.html

#ProofAssistant #Isabelle #Coq #Rocq #LCF #HOL

Functional Data Structures and Algorithms: a Proof Assistant Approach

https://fdsa-book.net/

#HackerNews #FunctionalDataStructures #Algorithms #ProofAssistant #Programming #HN

I worked through one possible solution to proving Pelletier's problem 24 in the #Mizar #proofassistant, but there are others.

#mathematics #logic #Mizar #proofassistant

https://thmprover.wordpress.com/2025/10/19/pelletiers-problem-24-in-mizar/

Despite the tornados and thunder storms, I wrote a brief "worked example" of how to prove one of Pelletier's problems in Mizar. This is part of the "Mizar 101" series of posts.

#Mizar #proofassistant #logic #mathematics

https://thmprover.wordpress.com/2025/10/14/schemas/

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

https://thmprover.wordpress.com/2025/10/11/how-to-check-you-installed-mizar-correctly/

I wrote a little about "literate programming" used to implement proof assistants, mostly about the "literate programming".

#LiterateProgramming #ProofAssistant #Logic #Mathematics

https://thmprover.wordpress.com/2025/09/16/literate-implementations-of-proof-assistants/