proof-automation

Lean 3's obsolete mathematical components library: please use mathlib4

Verification infrastructure for the Isabelle/HOL interactive proof assistant

⛏️ A refinement proof framework for haskell

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

Proof automation – for Agda, in Agda.

A web-based graphical proof assistant for LK and Hoare logic.

Ring, field, lra, nra, and psatz tactics for Mathematical Components

Micromega tactics for Mathematical Components

multi-logic proof generator

a linear logic prover based on Naoyuki Tamura's llprover that works under SWI Prolog

Library for formalizing cryptography proofs in Lean 3 (Deprecated)

Lean Optics provides an implementation of profunctor optics for Lean 4, featuring law-carrying composition, automated proof generation, and production-ready performance guarantees. Built on solid mathematical foundations, it offers a API for working with lenses, prisms, and traversals in functional programming.

The Open Deduction Proof Editor allows proof theorists (or anyone) to deconstruction proofs step by step. It currently supports deep inference formalisms, namely Open Deduction and naturally the Calculus of Structures. The front end of the application is written in Java, while the back end is written in Maude. There is also an implementation of …

A Lean 4 tactic library that simplifies category theory proofs using (co)Yoneda isomorphisms

Category Normal Form for Lean 4

An MCP server for deterministic probing and search of Lean 4 proof automation (Aesop / Grind).

Failed Lean proofs, classified and repaired. Search tactics stay out of the reviewed scripts.

Formal verification exercises in Coq: mechanized semantics, inductive proofs, custom automation, and verified parsers/automata

Brokers proof goals from Lean 4 and Rocq through a shared IR to SMT solvers, ATPs, and LLM provers, then verifies returned certificates and lifts proof terms back to the home system.