Mastodawn

New blog post: Introduction to Coinduction in Agda Part 1: Coinductive Programming

jesper.cx/posts/coinduction-part-1.html

#Agda #ProofAssistant #DependentTypes #Coinduction

Jesper Cockx - Introduction to Coinduction in Agda Part 1: Coinductive Programming

terrorist :: Feline Dec 24

**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

Department of Computer Science and Technology – Technical reports: UCAM-CL-TR-408

terrorist :: Feline Dec 15

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

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

50 years of proof assistants

Hacker News Nov 27

Functional Data Structures and Algorithms: a Proof Assistant Approach

https://fdsa-book.net/

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

Functional Data Structures and Algorithms. A Proof Assistant Approach

Alex Nelson Oct 19

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/

Pelletier’s Problem 24 in Mizar

There are probably several different ways to prove Pelletier’s Problem 24, so we will just investigate one way. Informal Roadmap for the Proof The first thing to do, whenever formalizing anyt…

Ariadne's Thread

Alex Nelson Oct 14

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/

Schemas and Proofs: A worked example

Today, we will work through proving one of Pelletier’s Seventy Five Problems for Testing Automated Theorem Provers. The focus will be on the proof of the claim. Then we will give several &#82…

Ariadne's Thread

Alex Nelson Oct 11

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/

How to check you installed Mizar correctly

We will be starting a “Mizar 101” series of posts, which will focus on “first steps in Mizar”. This post will discuss, among other things, “How to check you installed …

Ariadne's Thread

N-gated Hacker News Sep 17, 2025

🤓 Ah yes, the riveting saga of "normal-order syntax-rules" and the elusive call/cc fix-point, where syntax rules magically transform into a proof assistant. 🧙‍♂️ Because what better way to celebrate Daniel P. Friedman than with a marathon of indecipherable jargon and fewer common examples no one asked for. 🎉
https://okmij.org/ftp/Scheme/callcc-calc-page.html #normalordersyntax #syntaxrules #callcc #proofassistant #DanielPFriedman #programmingjargon #HackerNews #ngated

Normal-order syntax-rules and proving the fix-point of call/cc

CPS and beta-normalization with syntax-rules as a proof assistant in search of the fixpoint of call/cc

Alex Nelson Sep 16, 2025

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/

Literate Implementations of Proof Assistants

I have been experimenting with literate programming applied to the implementation of a toy HOL, and transcribing the Mizar proof assistant into Knuth’s WEB. This post will be more “prog…

Ariadne's Thread

José A. Alonso Aug 2, 2025

Readings shared August 1, 2025. https://jaalonso.github.io/vestigium/posts/2025/08/02-readings_shared_08-01-25 #Haskell #LeanProver #Math #ProofAssistant

Readings shared August 1, 2025

The readings shared in Bluesky on 1 August 2025 are Unconstrained optimization (in Isabelle/HOL). ~ Dustin Bryant. #ITP #IsabelleHOL #Math Seed-Prover: Deep and broad reasoning for automated theorem

Vestigium