Skip to content
View RexWzh's full-sized avatar

Highlights

  • Pro

Organizations

@JuliaImages @cubenlp @Lean-zh

Block or report RexWzh

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Maximum 250 characters. Please don't include any personal information such as legal names or email addresses. Markdown supported. This note will be visible to only you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
Showing results

An Open Source implementation of Notebook LM with more flexibility and features

TypeScript 19,610 2,189 Updated Feb 15, 2026

Lean formalizations of IMO problem statements

Lean 30 2 Updated Oct 23, 2025

SageMath integration for Lean4

Lean 10 Updated Nov 21, 2025

Lean Theorem Prover MCP

Python 271 38 Updated Feb 15, 2026

Litex is a simple formal language Learnable in 2 hours.

Go 653 8 Updated Jan 27, 2026

LeanArchitect extracts a blueprint directly from Lean source.

Lean 27 3 Updated Jan 27, 2026

Kimina Lean server (+ client SDK)

Python 180 26 Updated Jan 11, 2026

Formalisation of the Cambridge Part II and Part III courses Graph Theory, Combinatorics, Extremal and Probabilistic Combinatorics in Lean

Lean 74 17 Updated Jan 24, 2026

LeanInteract: A Python Interface for Lean 4

Python 102 8 Updated Jan 29, 2026

NeqLIPS: a powerful Olympiad-level inequality prover

Lean 39 2 Updated Sep 7, 2025

🤗 smolagents: a barebones library for agents that think in code.

Python 25,453 2,296 Updated Feb 15, 2026

A toy formally-specified Computer Algebra library written in Rust and formalized in Lean 4

Rust 22 1 Updated Jan 15, 2025

Emacs major mode for Lean 4

Emacs Lisp 121 37 Updated Jul 14, 2025

Examples using MetaProgramming for writing tactics etc.

Lean 20 3 Updated Nov 26, 2025

State-of-the-art bilingual open-sourced Math reasoning LLMs.

Python 539 36 Updated Oct 22, 2024

A simple REPL for Lean 4, returning information about errors and sorries.

Lean 188 66 Updated Jan 27, 2026

A Machine-to-Machine Interaction System for Lean 4.

Python 133 29 Updated Jan 15, 2026

Lean web editor

TypeScript 132 49 Updated Jan 6, 2026

A Lean 4 Jupyter kernel via repl

Python 35 3 Updated Nov 19, 2024

Catalog Of Math Problems Formalized In Lean

Lean 228 57 Updated Feb 15, 2026

A static analysis tool for Lean 4.

Lean 113 7 Updated Feb 12, 2026

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

Lean 213 32 Updated Jan 11, 2026

LLMs + Lean, on your laptop or in the cloud

Lean 202 31 Updated Oct 10, 2025

Wasm powered Jupyter running in the browser 💡

TypeScript 4,753 418 Updated Feb 11, 2026

Streamline your life using PromptingTools.jl, the Julia package that simplifies interacting with large language models.

Julia 164 23 Updated Feb 15, 2026

OpenAPI Generator allows generation of API client libraries (SDK generation), server stubs, documentation and configuration automatically given an OpenAPI Spec (v2, v3)

Java 25,818 7,386 Updated Feb 15, 2026

The Simple Agent Development Kit.

Python 1,318 114 Updated Aug 23, 2025

Natural Number Game

Lean 287 62 Updated Dec 27, 2025

Visualizing the network of math theories.

Python 603 50 Updated Jun 9, 2024
Next