A project to digitalise results from physics into Lean.

🎶 Explore Prolog coding with Vibe Prolog, a simple interpreter designed to run queries and demonstrate logic in programming efficiently.

🧩 Simplify your Prolog queries with qh2, a lightweight tool for enhancing query handling and improving logic programming efficiency.

🧠 Explore Prolog with sb0, a streamlined environment for developing logic-based applications and enhancing your programming skills.

🧠 Enhance logic programming with Prolog-KNE, a toolkit for knowledge extraction and natural language understanding in Prolog environments.

# Prime-Numbers Web AppThis web app helps users explore prime numbers through features like checking primality and generating sequences. With clear visuals and step-by-step explanations, it makes understanding prime numbers simple and engaging. 🐙✨

A template for blueprint-driven formalization projects in Lean.

ACL2 System and Books as Maintained by the Community

Solving Inequality Proofs with Large Language Models.

A Lean tactic for Canonical, a search procedure for terms in dependent type theory.

A Low Barrier Proof Assistant

CakeML: A Verified Implementation of ML

コード例で学ぶ Lean 言語

A Proof-oriented Programming Language

The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

Training an LLM to generate mathematical proofs with a formal verifier in Python

(Mirror) A Machine-to-Machine Interaction System for Lean 4

Experimental Lean 4 proof automation system using LLM-guided aesop tactic based strategies and logging successful hints for future annotations.

Formalizing Polynomial Commitment Schemes in the Interactive Theorem Prover Isabelle.

LeanDojo-v2 is an end-to-end framework for training, evaluating, and deploying AI-assisted theorem provers for Lean 4.