Stars
Lean 4 programming language and theorem prover
mattam82 / rocq
Forked from rocq-prover/rocqCoq 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 develo…
Open-source platform to build and deploy AI agent workflows.
🦛 CHONK docs with Chonkie ✨ — The lightweight ingestion library for fast, efficient and robust RAG pipelines
🌐 The open-source Agentic browser; privacy-first alternative to ChatGPT Atlas, Perplexity Comet, Dia.
HelixDB is an open-source graph-vector database built from scratch in Rust.
A lightweight next-gen data explorer - Postgres, MySQL, SQLite, MongoDB, Redis, MariaDB, Elastic Search, and Clickhouse with Chat interface
Agda is a dependently typed programming language / interactive theorem prover.
The most accurate document search and store for building AI apps
Open-source infrastructure for Computer-Use Agents. Sandboxes, SDKs, and benchmarks to train and evaluate AI agents that can control full desktops (macOS, Linux, Windows).
Mathematical Components compliant Analysis Library
Context retrieval for AI agents across apps and databases
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…
An open-source framework for verifiably private AI inference
A Python library for LLM-based evaluation using weighted rubrics.
Production-Ready MCP Server Framework • Build, deploy & scale secure AI agent infrastructure • Includes Auth, Observability, Debugger, Telemetry & Runtime • Run real-world MCPs powering AI Agents
Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
An MCP server that autonomously evaluates web applications.
Command-line program to download videos from YouTube.com and other video sites
JasonGross / coq
Forked from rocq-prover/rocqCoq 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 develo…
Using LLMs to transpile from Coq to Lean (public version, may be out of date)