Skip to content

README.adoc

Latest commit

 

History

History
48 lines (37 loc) · 1.37 KB

README.adoc

File metadata and controls

48 lines (37 loc) · 1.37 KB

nesy-solver

Public proof playground at nesy-solver.dev — submit proof obligations, get prover recommendations, stream verdicts back live.

Table of Contents

Overview

nesy-solver is the interactive frontend for the hyperpolymath neurosymbolic learning loop. It connects users directly to the Hypatia + Echidna + VeriSim pipeline:

  1. Submit a proof obligation in SMT-LIB, Lean 4, Coq/Rocq, Idris2, or Agda

  2. The app recommends a prover strategy based on live proof_attempts data in VeriSim

  3. Dispatches to Echidna for execution

  4. Streams the verdict back in real time

  5. Records the attempt in verisim-api — the playground improves its recommendations over time from actual usage data

Supported Formalisms

  • SMT-LIB (Z3, CVC5)

  • Lean 4

  • Coq / Rocq

  • Idris2

  • Agda

Architecture

Component Role

web/

Frontend (ReScript + Deno)

src/core/

Proof dispatch and strategy selection

src/interface/abi/

Idris2 ABI for prover interface contracts

src/interface/ffi/

Zig FFI bridge to Echidna + external provers

deploy/

Container deployment (Containerfile, Podman)

verisim-api

External: records proof attempts, drives strategy recommendations

License

MPL-2.0. See LICENSE.