Step-by-step proof for equivalence in propositional logic and ND prover for first-order logic.

A program that verifies proofs in the F0 proof system

Automated theorem proving, Logic Programming, Optimization examples.

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

Code and data for paper "Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving"

solving-satisfaction-problems-with-theorem-provers

a constraint-based syntax-guided synthesis (SyGuS) engine

multi-logic proof generator

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

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

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

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

quick and dirty theorem prover

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

"Natural" Natural Deduction: a Theorem Prover for Propositional Logic

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

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

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.

A Lean nightly installer for CSE 505.

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