proof-automation 开源项目推荐（23 个）

leanprover-community /mathlib3

Lean 3 已废弃的数学组成部分库：请使用 mathlib4

awslabs /AutoCorrode

Verification infrastructure for the Isabelle/HOL interactive proof assistant

TOTBWF /refinery

⛏️ A refinement proof framework for haskell

uwplse /PUMPKIN-PATCH

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

wenkokke /AutoInAgda

Proof automation – for Agda, in Agda.

proof-tree-builder /proof-tree-builder.github.io

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

math-comp /mczify

Micromega tactics for Mathematical Components

marnix /zigmmverify

该项目在 GitHub 上没有填写描述

owings1 /pytableaux

multi-logic proof generator

wenkokke /swillprover

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

dtumad /lean-crypto-formalization

Library for formalizing cryptography proofs in Lean 3 (Deprecated)

fraware /lean-optics

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.

joe-lynch /ODPE

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 …

fraware /lean-yo

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

stuff-of-awe /awesome-z3

Practical Z3 resources for the mathematics and verification communities.

fraware /lean-cat-nf

Category Normal Form for Lean 4

padieul /lean-proof-auto-mcp

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

SaharRamezani /Coq-Learning

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

pavanamthomas /lean4-automation-debugging

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

vince-gonzalez /mmforge

Find avoidable axiom dependencies in Metamath databases, and build the proofs that remove them. Nine contributions merged into set.mm.