Lists (4)
Starred repositories
A flagship 560-billion-parameter open-source MoE model that advances Native Formal Reasoning in Lean4 through agentic tool-integrated reasoning.
Asterinas aims to be a production-grade Linux alternative—memory safe, high-performance, and more.
Microkernel-Based Research Operating System Written in Rust
OpenSeeker: A search agent with open-source data and models
Elevate your AI research writing, no more tedious polishing ✨
ARIS ⚔️ (Auto-Research-In-Sleep) — Lightweight Markdown-only skills for autonomous ML research: cross-model review loops, idea discovery, and experiment automation. No framework, no lock-in — works…
AI agents running research on single-GPU nanochat training automatically
A Lean4 script for robustly verifying submitted proofs of theorems and implementations of functions
The Cloud Sandbox Built for AI Agents
Lean 4 theorem proving skill and workflow pack for AI coding agents
Verified interval arithmetic for Lean 4 — prove bounds on exp, sin, cos, find roots, all machine-checked
Formalizing the stable marriage problem and the Gale-Shapley algorithm in Lean
Machine Leanring for Mini Lang, Mini Lang for Machine Learnining
Minimal open-source implementation of AlphaProof and HyperTree Proof Search.
LeanInteract: A Python Interface for Lean 4
A Machine-to-Machine Interaction System for Lean 4.
Running Aristotle from Harmonic on Putnam 2025 problems
Formally proving the security of Fast Reed-Solomon interactive oracle proofs of proximity
A tool to auto-generate and render slides from Markdown comments in the Lean editor.
ThetaEvolve: Test-time Learning on Open Problems, enabling RL training on AlphaEvolve/OpenEvolve and emphasizing scaling test-time compute