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

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

LeanInteract: A Python Interface for Lean 4

A template for blueprint-driven formalization projects in Lean.

Solving Inequality Proofs with Large Language Models.

A Low Barrier Proof Assistant

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

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

A Machine-to-Machine Interaction System for Lean 4.

Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs

An API for interfacing with Coq through Tactician by external agents

Tool for data extraction and interacting with Lean programmatically.

Four color theorem, Guthrie, Kempe, Tait and other people and stuff

📐 Natural language explanations of Lean 4 theorems | MathJax 4.0 rendering • Batch processing • Mathematical notation | Formal verification accessibility

Tiny theorem prover with syntax like Lean 4 in <1K LOC

Implementation and subsequent optimization for "Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models"

🔍A deep dive into Formal Methods in Software Engineering 📜—exploring automata, logic, verification, and specification techniques to ensure software correctness and reliability.

Python Symbolic Information Theoretic Inequality Prover

Jumla is a Python package for generating Lean 4 formal verification tasks from Python specifications.

This repository contains the code, data generation scripts, and documentation for a computational study exploring the relationships between the cuteness level of anime profile pictures, the beard prominence of users, and the probability that a user is actually a medieval fantasy dwarf.