Kaiyu Yang

Tool for data extraction and interacting with Lean programmatically.

LLMs as Copilots for Theorem Proving in Lean

No description.

No description.

An implementation of Color2Gray with convolutional neural networks

No description.

NeurIPS 2023 Tutorial on Machine Learning for Theorem Proving

A simple wrapper to run multiple SMT solvers in parallel

No description.

No description.

Code for LeanDojo's website

A WebUI for Efficient Fine-Tuning of 100+ LLMs (ACL 2024)

No description.

A collection of the newest Claude Code open source

A formal proof of the Riemann Hypothesis for curves

No description.

Lean formalizations of IMO problem statements

An evaluation benchmark for undergraduate competition math in Lean4, Isabelle, Coq, and natural language.

A collection of formalized statements of conjectures in Lean.

No description.

No description.

SGLang is a fast serving framework for large language models and vision language models.

This dataset code generates mathematical question and answer pairs, from a range of question types at roughly school-level difficulty.

Scientific computing in Lean 4

A Survey on Deep Learning for Theorem Proving

The user home repository for the Mathematics in Lean tutorial.

No description.

Soufflé

🤗 Transformers: State-of-the-art Machine Learning for Pytorch, TensorFlow, and JAX.

🤗 The largest hub of ready-to-use datasets for ML models with fast, easy-to-use and efficient data manipulation tools

https://yangky11.github.io/

An opinionated code formatter for Julia. Plot twist - the opinion is your own.

MiroThinker is a deep research agent optimized for complex research and prediction tasks. Our latest models, MiroThinker-1.7 and MiroThinker-H1, achieve 74.0 and 88.2 on the BrowseComp, respectively.

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

No description.

Bijection datatype for Julia.

Tactics for discharging Lean goals into SMT solvers.

An updated version of miniF2F with lots of fixes and informal statements / solutions.

Coq Protocol Playground with Se(xp)rialization of Internal Structures.

[NeurIPS 2024] Efficient LLM Scheduling by Learning to Rank

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

A high-throughput and memory-efficient inference and serving engine for LLMs

A high-level API for interacting with SMT solvers.

No description.

SciGLM: Training Scientific Language Models with Self-Reflective Instruction Annotation and Tuning

No description.

Code repo for MathAgent

No description.

White-box automation for Lean 4

The math library of Lean 4

Benchmark for undergraduate-level formal mathematics

An experimental open-source attempt to make GPT-4 fully autonomous.

😎 A curated list of awesome GitHub Profile READMEs 📝

An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.

No description.

No description.

No description.

Lean 4 build system and package manager with configuration files written in Lean.

Some Lean tutorials

No description.

Proof recording for Lean 3

Proof artifact co-training for Lean

EMNLP'2021: SimCSE: Simple Contrastive Learning of Sentence Embeddings

No description.

Princeton University Ph.D. Dissertation Template

A documentation generator for Julia.

Sets of scripts for generating procedural 3D bottles done in Blender using Python

A general-purpose probabilistic programming system with programmable inference

Comparing fairness-aware machine learning techniques.

Collection of builder repositories for BinaryBuilder.jl

Python libraries for Google Colaboratory

Hydra is a framework for elegantly configuring complex applications

Repository to track the progress in Natural Language Processing (NLP), including the datasets and the current state-of-the-art for the most common NLP tasks.

Example pybind11 module built with a CMake-based build system

No description.

Seq2Tree model for Solving Math Word Problems

Tips for releasing research code in Machine Learning (with official NeurIPS 2020 recommendations)

Neural Adobe-UCSD Parser, the current State of the Art in Constituency and Dependency Parsing.

Source code for "Head-Driven Phrase Structure Grammar Parsing on Penn Treebank" published at ACL 2019

High-accuracy NLP parser with models for 11 languages.

A microframework for working with Amazon's Mechanical Turk

Template of Coq Plugin using the Dune build system, and showcasing some advanced features

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

The world's simplest facial recognition api for Python and the command line

The Jinja2 template engine

Lightweight, configurable Sphinx theme. Now the Sphinx default!

Deep universal probabilistic programming with Python and PyTorch

Coq is a formal proof management system. 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.

Type-driven code generation for OCaml >=4.02

No description.

Deformable Convolutional Networks + MST + Soft-NMS

This project is part of the course EECS 573 in Fall 2016. This project included a comprehensive errata database for some of the ARM cores, that can be used directly. Other experiments focus on mining hardware errata to gain insight into relations between keywords and manufacturers/cores.

Convolutional neural network model for video classification trained on the Kinetics dataset.

Detecting Visual Relationships with Deep Relational Networks

No description.

Pytorch implementation of "A simple neural network module for relational reasoning" (Relational Networks)

No description.

http://torch.ch

Computation using data flow graphs for scalable machine learning

A tensorflow implementation of Deep Convolutional Generative Adversarial Networks

MS COCO API - http://mscoco.org/

Deep Convolutional Generative Adversarial Networks

Code to test and use the model from "Stacked Hourglass Networks for Human Pose Estimation"