#mizar — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #mizar, aggregated by home.social.
-
Mizar: the first usable proof assistant for mathematics. ~ Lawrence Paulson. https://lawrencecpaulson.github.io//2026/05/07/Mizar.html #Mizar #ATP #Math
-
Readings shared March 14, 2026. https://jaalonso.github.io/vestigium/posts/2026/03/15-readings_shared_02-14-26 #AI #Agda #ITP #LeanProver #Math #Mizar
-
130k lines of formal topology in two weeks: Simple and cheap autoformalization for everyone? ~ Josef Urban. https://arxiv.org/abs/2601.03298v1 #ITP #Mizar #LLMs #Math #Autoformalization
-
130k lines of formal topology in two weeks: Simple and cheap autoformalization for everyone? ~ Josef Urban. https://arxiv.org/abs/2601.03298v1 #ITP #Mizar #LLMs #Math #Autoformalization
-
130k lines of formal topology in two weeks: Simple and cheap autoformalization for everyone? ~ Josef Urban. https://arxiv.org/abs/2601.03298v1 #ITP #Mizar #LLMs #Math #Autoformalization
-
130k lines of formal topology in two weeks: Simple and cheap autoformalization for everyone? ~ Josef Urban. https://arxiv.org/abs/2601.03298v1 #ITP #Mizar #LLMs #Math #Autoformalization
-
130k lines of formal topology in two weeks: Simple and cheap autoformalization for everyone? ~ Josef Urban. https://arxiv.org/abs/2601.03298v1 #ITP #Mizar #LLMs #Math #Autoformalization
-
1000+ theorems (The spiritual successor of Freek’s list of 100 theorems. Now with more than 1000 theorems!). ~ Katja Berčič et als. https://1000-plus.github.io/all #Math #ITP #IsabelleHOL #HOL_Light #Rocq #LeanProver #Metamath #Mizar
-
Readings shared October 20, 2025. https://jaalonso.github.io/vestigium/posts/2025/10/21-readings_shared_10-20-25 #ACL2 #Autoformalization #FunctionalProgramming #Haskell #ITP #LLMs #LeanProver #Logic #Math #Mizar #RustLang
-
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
-
Readings shared September 6, 2024. https://jaalonso.github.io/vestigium/posts/2024/09/06-readings_shared_09-06-24 #ITP #LeanProver #Lean4 #IsabelleHOL #Coq #Agda #PVS #Logic #HOL4 #Lisa #Mizar #ACL2 #Math #AI #MachineLearning
-
Lecturas compartidas el 11 de mayo de 2024. https://jalonso.substack.com/lecturas-compartidas-el-11-de-mayo #ITP #Lean4 #IsabelleHOL #Agda #Coq #HOL_Light #Metamath #Mizar #Math #Programming #CommonLisp
-
Algorithm and abstraction in formal mathematics. ~ Heather Macbeth. https://arxiv.org/abs/2405.04699 #ITP #Agda #Coq #Lean4 #HOL_Light #IsabelleHOL #Metamath #Mizar #Math