-
Harvard University
- Cambridge, MA
- http://namin.org
Stars
- All languages
- Agda
- Assembly
- Awk
- Bluespec
- C
- C#
- C++
- CSS
- CWeb
- Clojure
- CoffeeScript
- Common Lisp
- Coq
- Dafny
- Elm
- Emacs Lisp
- Erlang
- F*
- Forth
- Fortran
- Go
- HTML
- Haskell
- Idris
- Isabelle
- Java
- JavaScript
- JetBrains MPS
- Julia
- Jupyter Notebook
- Kotlin
- Lean
- Lua
- Makefile
- Markdown
- NewLisp
- OCaml
- Objective-C
- Pascal
- Perl
- Prolog
- Pure Data
- Python
- R
- Racket
- Rascal
- Ruby
- Rust
- SCSS
- SMT
- SWIG
- Scala
- Scheme
- Shell
- Slash
- Smarty
- Standard ML
- Swift
- TeX
- TypeScript
- UrWeb
- VHDL
- Verilog
- Vue
🕸 WebGL Graph Visualizations for React. Maintained by @goodcodeus.
A JavaScript library aimed at visualizing graphs of thousands of nodes and edges
Files associated with the course Interactive Theorem Proving at LMU SoSe 2025
LLM-based ontological extraction tools, including SPIRES
First-order logic theorem prover supporting unification with approximate vector similarity
Experiments in automation for Lean
A verifier for automated and interactive proofs about transition systems. This repository is a public mirror with stable development snapshots. Submit issues and PRs here.
Python client to interact with the lean4 language server.
Translating humaneval into dafny
The official implementation of "Self-play LLM Theorem Provers with Iterative Conjecturing and Proving"
TxAgent: An AI Agent for Therapeutic Reasoning Across a Universe of Tools
Proof assistant based on the λΠ-calculus modulo rewriting
Canonical is a performant sound and complete type inhabitation solver for dependent type theory.
A Lean tactic for Canonical, a search procedure for terms in dependent type theory.
Implementation of the λΠ-calculus modulo rewriting
MLX Omni Server is a local inference server powered by Apple's MLX framework, specifically designed for Apple Silicon (M-series) chips. It implements OpenAI-compatible API endpoints, enabling seaml…
Browser MCP is a Model Context Provider (MCP) server that allows AI applications to control your browser
A simple adapter to convert a MCP server to a GPT actions compatible API
Source code for the Mathematics in Lean tutorial.
An MCP server that autonomously evaluates web applications.
piggy-backing on the Dafny language implementation to explore interactive semi-automated verified program synthesis, combining LLMs and symbolic reasoning
The Platform for Self-Improving Code. Ideal for GPU kernels, ML model development, feature engineering, prompt engineering, and other optimizable code.
An MCP server that lets you interact with LSP servers