#mizar — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #mizar, aggregated by home.social.
-
Mizar (2017)
Un mio vecchio brano scritto in linguaggio Csound 5.11 nel 2017.
#csound #computermusic #spectrogram #mizar #mattiagiovanetti
-
Mizar (2017)
Un mio vecchio brano scritto in linguaggio Csound 5.11 nel 2017.
#csound #computermusic #spectrogram #mizar #mattiagiovanetti
-
Reformalization of the Jordan curve theorem. ~ Simon Guilloud, Sankalp Gambhir, Samuel Chassot. https://openreview.net/pdf?id=jhbkIZOn5a #Mizar #LeanProver #HOL_Light #Agda #ITP
-
Reformalization of the Jordan curve theorem. ~ Simon Guilloud, Sankalp Gambhir, Samuel Chassot. https://openreview.net/pdf?id=jhbkIZOn5a #Mizar #LeanProver #HOL_Light #Agda #ITP
-
Mizar: the first usable proof assistant for mathematics. ~ Lawrence Paulson. https://lawrencecpaulson.github.io//2026/05/07/Mizar.html #Mizar #ATP #Math
-
Mizar: the first usable proof assistant for mathematics. ~ Lawrence Paulson. https://lawrencecpaulson.github.io//2026/05/07/Mizar.html #Mizar #ATP #Math
-
2026-04-24T19:37:51+09:00:00
ミザール Mizar おおぐま座ζ ζUMa
赤経13h23m56s 赤緯54°55'.5
距離78光年 実視等級2.06d（重星）
北斗七星のひしゃくの柄の端から2番目の星、2等星のミザールと4等星のアルコルは、目の良い人なら肉眼で見える2重星です。
#ミザール #天体観測 #mizar #photography #fedibird -
2026-04-24T19:37:51+09:00:00
ミザール Mizar おおぐま座ζ ζUMa
赤経13h23m56s 赤緯54°55'.5
距離78光年 実視等級2.06d（重星）
北斗七星のひしゃくの柄の端から2番目の星、2等星のミザールと4等星のアルコルは、目の良い人なら肉眼で見える2重星です。
#ミザール #天体観測 #mizar #photography #fedibird -
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
-
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
-
Formalization of separable version of Banach–Alaoglu theorem. ~ Hiroyuki Okazaki, Takehiko Mieno. https://reference-global.com/download/article/10.2478/forma-2025-0018.pdf #Mizar #ITP #Math
-
Formalization of separable version of Banach–Alaoglu theorem. ~ Hiroyuki Okazaki, Takehiko Mieno. https://reference-global.com/download/article/10.2478/forma-2025-0018.pdf #Mizar #ITP #Math
-
Formalization of Wallis infinite product formula for π and the Wallis integral. ~ Yasushige Watase. https://reference-global.com/download/article/10.2478/forma-2025-0007.pdf #Mizar #ITP #Math
-
Formalization of Wallis infinite product formula for π and the Wallis integral. ~ Yasushige Watase. https://reference-global.com/download/article/10.2478/forma-2025-0007.pdf #Mizar #ITP #Math
-
A formal proof of Stirling’s formula. ~ Yasushige Watase. https://reference-global.com/download/article/10.2478/forma-2025-0008.pdf #Mizar #ITP #Math
-
A formal proof of Stirling’s formula. ~ Yasushige Watase. https://reference-global.com/download/article/10.2478/forma-2025-0008.pdf #Mizar #ITP #Math
-
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
-
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
-
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
-
Pelletier’s problem 24 in Mizar. ~ Alex Nelson. https://thmprover.wordpress.com/2025/10/19/pelletiers-problem-24-in-mizar/ #ITP #Mizar #Logic #Math
-
Pelletier’s problem 24 in Mizar. ~ Alex Nelson. https://thmprover.wordpress.com/2025/10/19/pelletiers-problem-24-in-mizar/ #ITP #Mizar #Logic #Math
-
Redefinitions in Mizar. ~ Alex Nelson. https://thmprover.wordpress.com/2025/06/24/redefinitions-in-mizar/ #ITP #Mizar #Math
-
Readings shared June 22, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/23-readings_shared_06-22-25 #ITP #Mizar #Math
-
Surreal dyadic and real numbers: A formal construction (in Mizar). ~ Karol Pąk. https://mizar.uwb.edu.pl/fm/fm33/surrealn.pdf #ITP #Mizar #Math
-
Surreal numbers: A study of square roots (in Mizar). ~ Karol Pąk. https://mizar.uwb.edu.pl/fm/fm33/surreals.pdf #ITP #Mizar #Math
-
Free product of groups (in Mizar). ~ Sebastian Koch. https://mizar.uwb.edu.pl/fm/fm33/gr_free0.pdf #ITP #Mizar #Math
-
Application of complex classes to number theory (in Mizar). ~ Rafał Ziobro. https://mizar.uwb.edu.pl/fm/fm33/newton06.pdf #ITP #Mizar #Math
-
Conway’s normal form in the Mizar system. ~ Karol Pąk. https://mizar.uwb.edu.pl/fm/fm33/surrealc.pdf #ITP #Mizar #Math
-
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