## proofwidgets

Helper toolkit for creating your own Lean 4 UserWidgets

**1-20**of

**91**packages depending on

**leanprover-community/proofwidgets**

Sort by

Package Name

### lindy-labs/aegis

uses`v0.0.39`

Verify Cairo contracts in Lean 4### FR-vdash-bot/algorithm

uses`v0.0.42`

Verified efficient algorithms in Lean4.### jsm28/AM

uses`v0.0.42`

Lean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib)### dwrensha/animate

uses`v0.0.41`

tool for turning Lean proofs into Blender animations### mseri/BET

uses`v0.0.42`

Project for "Machine-Checked Mathematics" at the Lorentz Center### fpvandoorn/bonnAnalysis

uses`v0.0.39`

repository for the collaborative formalization seminar in Analysis in Bonn### jaalonso/Calculemus2

uses`v0.0.42`

Proof exercises in Lean4 and Isabelle/HOL### jaalonso/Calculemus2_es

uses`v0.0.42`

Ejercicios de demostraciĆ³n con Lean4 e Isabelle/HOL.### fpvandoorn/carleson

uses`v0.0.42`

A formalized proof of Carleson's theorem in Lean### knowsys/certifyingDatalog

uses`v0.0.41`

A certified checker for Datalog entailments, written in Lean### YaelDillies/ChandraFurstLipton

uses`v0.0.42`

Formalisation in the Lean theorem prover of the relation between corner-free sets and communication complexity### anlucia/chromatic_polynomial

uses`v0.0.41`

Chromatic polynomial in Lean4### RemyDegenne/clt

uses`v0.0.42`

Central limit theorem in Lean### morganfshirley/CommComp

uses`v0.0.42`

Formalization of communication complexity in Lean### dwrensha/compfiles

uses`v0.0.42`

Catalog Of Math Problems Formalized In Lean### leanprover-community/ConNF

uses`v0.0.42`

A formal consistency proof of Quine's set theory New Foundations### optsuite/convex

uses`v0.0.39`

### lindy-labs/corelib_verification

uses`v0.0.39`

### Shreyas4991/DGAlgorithms

uses`v0.0.40`

Distributed Graph Algorithms in Lean### madvorak/duality

uses`v0.0.41`

Duality theory in linear optimization and its extensions