Lean binding for libpq

The Agda Universal Algebra Library (html docs available at the url below)

DenkiChip (でんきチップ) is a compact and bold Japanese pixel font under SIL OFL 1.1

A formalization of PCF theory in lean

Lean library for Universal Algebra

直観主義の命題論理+自然演繹の中で与えられた定理を検証する遺伝的アルゴリズムを用いた証明探索エンジン

Category theory but for kitty cats, meow 🐱🐈

forked from muhokama/ring

Lean formalization of selected lemmas from "Term Rewriting and All That"

HOL-Light Library for Modal Systems

A List of Dirty, Naughty, Obscene and otherwise Bad Words

A library of mechanised undecidability proofs in the Coq proof assistant.

Linearizability Hoare Logic

Converts LaTeX tags to unicode: \mathcal{H} → ℋ. Available on the web or as Automator script for the Mac.

A Git-compatible VCS that is both simple and powerful

First order model theory inside a topos in Lean

This app twXiv gives arXiv daily new submissions by tweets. We use python3 scripts. twXiv is not affiliated with arXiv.

A repo to document candidate solutions for Erdős problems produced via LLM-driven proof search.

Lean4 formalization of "A Simplified Round-by-round Soundness Proof of FRI"