stanford-centaur/PyPantograph

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

Language: Python - Size: 46.8 MB - Last synced at: 6 days ago - Pushed at: 11 days ago - Stars: 80 - Forks: 18

vladimir-skvortsov/ontol

A tool for parsing and visualizing ontology files written in the Ontol DSL

Language: Python - Size: 876 KB - Last synced at: 22 days ago - Pushed at: 23 days ago - Stars: 4 - Forks: 1

konstantinosKokos/quill

🪶 Neural premise selection for Agda.

Language: Python - Size: 3.33 MB - Last synced at: 2 months ago - Pushed at: 4 months ago - Stars: 2 - Forks: 0

HOLMS-lib/HOLMS

HOL-Light Library for Modal Systems

Language: OCaml - Size: 212 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 1 - Forks: 0

Eleanor-H/MUSTARD

Code & data for ICLR 2024 spotlight paper: 🍯MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data

Language: C++ - Size: 21 MB - Last synced at: 4 months ago - Pushed at: 12 months ago - Stars: 38 - Forks: 1

HOLMS-lib/holms-lib.github.io

HOL Light Library for Modal Systems

Size: 96.7 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 0 - Forks: 0

j991222/ai4math-papers

AI for Mathematics (AI4Math) paper list

Size: 51.8 KB - Last synced at: 5 months ago - Pushed at: 8 months ago - Stars: 135 - Forks: 8

amka66/mai

mai: MAth Interpreter with Standard Foundations

Language: Prolog - Size: 177 KB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 4 - Forks: 1

MarcinBrojek/log-FO-prover

A tool for automatically verifying whether a given first-order logic formula is a tautology, based on Herbrand's theory and the Davis-Putnam SAT solver. Implemented in C++.

Language: C++ - Size: 10.7 KB - Last synced at: about 2 months ago - Pushed at: 10 months ago - Stars: 0 - Forks: 0

lambduli/resin

A toy Automated Theorem Prover for First Order Classical Logic built on Resolution.

Language: Haskell - Size: 264 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 1 - Forks: 0

philzook58/pyvampire

A simple repackaging of the Vampire automated theorem prover

Language: Shell - Size: 20.8 MB - Last synced at: 3 months ago - Pushed at: about 1 year ago - Stars: 1 - Forks: 0

auntyellow/math

Brute force math problem solving

Language: Python - Size: 5.96 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 6 - Forks: 1

filipbartek/learning-precedences-from-elementary-symbol-features

Language: TeX - Size: 280 KB - Last synced at: almost 2 years ago - Pushed at: over 4 years ago - Stars: 0 - Forks: 0

elizabeth-c-chen/data1030-ML-theorem-proving

Course Project for Hands-on Data Science (DATA 1030) at Brown University. View project at elizabethchen.works/data1030!

Language: Jupyter Notebook - Size: 238 MB - Last synced at: about 2 years ago - Pushed at: about 3 years ago - Stars: 0 - Forks: 0

jaalonso/Razonando-con-Lean

Elaboración de demostraciones con Lean.

Language: Lean - Size: 43 KB - Last synced at: about 2 months ago - Pushed at: almost 3 years ago - Stars: 1 - Forks: 0

artemmavrin/autoproof

Intuitionistic and classical propositional logic library

Language: Haskell - Size: 5.3 MB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 1 - Forks: 0

cluesurfback/math

Math in XO

Size: 22.5 KB - Last synced at: about 1 month ago - Pushed at: almost 4 years ago - Stars: 0 - Forks: 0