Skip to content

@project-numina project-numina

All

    Repositories list

    20 repositories

    • fuse-desktop

      Public
      Fuse: a desktop workspace for Lean formalization with AI agents
      TypeScript
      •
      GNU Affero General Public License v3.0
      •1•9•0•0•Updated Oct 4, 2026Oct 4, 2026

    • kakeya-3d

      Public
      Lean
      •
      Apache License 2.0
      •4•31•0•0•Updated Sep 9, 2026Sep 9, 2026

    • LeanTriathlon

      Public
      Lean
      •
      Apache License 2.0
      •2•9•0•3•Updated Aug 30, 2026Aug 30, 2026

    • numina-lean-agent

      Public
      Python
      •34•279•1•14•Updated Jul 8, 2026Jul 8, 2026

    • feynman-bench

      Public
      Open benchmark for Feynman IBP integral-reduction solvers
      Python
      •
      MIT License
      •0•2•0•0•Updated May 26, 2026May 26, 2026

    • BrascampLieb

      Public
      A Lean4 repository for formalization of results from "Effective Brascamp-Lieb Inequalities"
      Lean
      •0•0•0•0•Updated Apr 10, 2026Apr 10, 2026

    • lean-lsp-mcp

      Public
      Python
      •
      MIT License
      •4•21•2•2•Updated Mar 11, 2026Mar 11, 2026

    • lean-explore

      Public
      A search engine for Lean 4 declarations for numina
      Python
      •
      Apache License 2.0
      •14•0•1•0•Updated Jan 29, 2026Jan 29, 2026

    • Numina-Putnam2025

      Public
      Lean
      •
      MIT License
      •0•5•0•0•Updated Jan 20, 2026Jan 20, 2026

    • kimina-lean-server

      Public
      Kimina Lean server (+ client SDK)
      repllean4
      repllean4
      Python
      •
      MIT License
      •38•212•7•6•Updated Jan 11, 2026Jan 11, 2026

    • LeanGeo

      Public
      Solving Competition Geometry Problems in Lean
      Lean
      •
      MIT License
      •5•44•1•0•Updated Aug 26, 2025Aug 26, 2025

    • verl

      Public
      verl: Volcano Engine Reinforcement Learning for LLMs
      Python
      •
      Apache License 2.0
      •4.7k•0•0•7•Updated Aug 18, 2025Aug 18, 2025

    • kimina-prover-rl

      Public
      Kimina-Prover RL pipeline
      Python
      •
      Apache License 2.0
      •4.7k•12•0•0•Updated Aug 14, 2025Aug 14, 2025

    • LeanEuclid

      Public
      LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.
      Lean
      •
      MIT License
      •20•1•0•1•Updated May 31, 2025May 31, 2025

    • annotation-guidelines

      Public
      Lean
      •1•3•1•0•Updated May 29, 2025May 29, 2025

    • combinatorics

      Public
      A Lean 4 library on combinatorics as an enhancement to mathlib4.
      Lean
      •
      Apache License 2.0
      •0•1•12•5•Updated Apr 27, 2025Apr 27, 2025

    • IMO-Steps

      Public
      Lean
      •
      MIT License
      •4•1•0•0•Updated Mar 13, 2025Mar 13, 2025

    • lean-exemples

      Public
      Lean
      •0•3•0•0•Updated Jan 23, 2025Jan 23, 2025

    • mathlib4

      Public
      The math library of Lean 4
      Lean
      •
      Apache License 2.0
      •1.7k•0•0•0•Updated Dec 20, 2024Dec 20, 2024

    • aimo-progress-prize

      Public
      Jupyter Notebook
      •
      Apache License 2.0
      •35•496•6•0•Updated Jul 22, 2024Jul 22, 2024
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.