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

https://lispy-gopher-show.itch.io/lispmoo2/devlog/1481398/homespun-acl2-handler-bind-condition-handling

#acl2 simple introduction to acl2 for the #commonLisp inclined.

loop$, apply$, thms oh my.

In particular, I implement a model of a simple case of the common lisp condition system that is directly compatible with both ansi common lisp and acl2. (a computational logic for applicative common lisp).

#firstOrderLogic #theoremProving #programming #logic #example

Technically this is in support of my lisp / moo compatibility layer but I am not going to beleaguer the tag.

RE: https://floss.social/@alcinnz/116319031843948749

About programming explicitly, the US tax code implicitly, and the difficulty of translating natural and legal language into simple… anything, really; code, webpages, outcomes.

Waving my hands at *two* things I know nothing about: has anyone translated any tax code into a theorem prover? #TheoremProving

Want to learn more about the latest developments on using AI and (interactive) theorem proving in Mathematics? Wait no longer!

We have a great line-up of speakers at our online Workshop on AI and Theorem Provers in Mathematics. The workshop will be held online from 8th to 10th of April and attendance is free (registration required). For more details, visit the workshop website: https://aitpm.github.io/

#math #itp #theoremProving #isabelleHOL #lean #llm #ai #formal_mehods #agda #hol #mathematics

Mehtaab Sawhney (@mehtaab_sawhney)

OpenAI 내부 모델이 수학 문제 'Erdos #846'의 증명을 생성해 논문으로 공개됐습니다(링크 포함). 해당 문제는 기존 문헌에서 파생될 수도 있지만, 내부 모델이 직접 증명을 도출한 사례라는 점에서 주목받고 있습니다. 작성자는 모델의 증명을 보고 감탄했다고 언급했습니다.

https://x.com/mehtaab_sawhney/status/2026716221933343147

#openai #theoremproving #airesearch #mathematics

Terminal now can help you with formal proofs and theorem provers 🤯

📐 **lean-tui** — A TUI for visualizing Lean programs and proofs

💯 Live proof trees, data/effect flow views & real-time updates from your editor

🦀 Written in Rust & built with @ratatui_rs

⭐ Source: https://codeberg.org/wvhulle/lean-tui

#rustlang #ratatui #tui #lean #theoremproving #cli #devtools #terminal

Kimon Fountoulakis (@kfountou)

작성자는 모델이 기존 논증의 짧은 연쇄를 올바르게 결합해 내는 능력을 과소평가하지 않으며, 이는 인상적이고 수학자들의 작업 방식을 바꿀 것이라 말합니다. 다만 이러한 성과가 인간이 믿었던 것처럼 문제들이 본질적으로 훨씬 더 어렵다는 관점의 정당성을 완전히 입증하는지는 불확실하다고 지적합니다.

https://x.com/kfountou/status/2022671762173854080

#ai #theoremproving #automatedreasoning #research