A math expression evaluation library for rust

egg is a flexible, high-performance e-graph library

A project to map out the relations between different equational theories of Magmas.

A modern computer algebra library for Python and Rust.

Official code for paper: INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving

Cylindrical algebraic decomposition in pure Python (SymPy)

Summing squares in Lean

Automatic sum of square representation calculator. Symbolic SOStool with graphic user interface.

Decompose a rational polynomial exactly as a sum-of-squares if possible

A simple Maple program for expressing 3-variable symmetric polynomials of degree six as Sum of Squares (SOS) form.

Python implementation of Sum-of-Squares optimization built on picos

[ICLR 2024] SWE-bench: Can Language Models Resolve Real-world Github Issues?

We provide a dataset of equations represented as PNG-images and Latex code. This dataset is useful for learning to detect similarities in equations.

Learning to Perform Local Rewriting for Combinatorial Optimization

LLMs as Copilots for Theorem Proving in Lean

LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.

Code for the paper: Proving Theorems Recursively

Files for CADassistant program - part of my PhD work.

Files and tools for SMT-COMP, the International Satisfiability Modulo Theories Competition.

Inference Llama 2 in one file of pure C

This project proposes two Reinforcement Learning (RL) approaches combined with Graph Neural Networks (GNN) for Suggesting Variable Order (SVO).

[COLM 2024] A Survey on Deep Learning for Theorem Proving

A Foreign Function Interface (FFI) to cvc5 solver in Lean.

pySMT: A library for SMT formulae manipulation and solving