nesy-solver/index.html at main · hyperpolymath/nesy-solver · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
<!-- SPDX-License-Identifier: MPL-2.0 -->
<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
<!DOCTYPE html>
<html lang="en">
<head>
  <meta charset="UTF-8" />
  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>nesy-solver — Neurosymbolic Proof Playground</title>
  <meta name="description" content="Live proof playground for neurosymbolic theorem provers, backed by a learning loop across hypatia, echidna, and verisimdb." />
  <link rel="stylesheet" href="/public/styles.css" />
</head>
<body data-theme="dark">
  <header class="site-header">
    <div class="brand">
      <h1>nesy-solver</h1>
      <span class="tagline">neurosymbolic proof playground</span>
    </div>
    <nav class="site-nav">
      <a href="#playground" class="nav-link active">Playground</a>
      <a href="#strategy" class="nav-link">Strategy</a>
      <a href="#certificates" class="nav-link">Certificates</a>
      <a href="#about" class="nav-link">About</a>
    </nav>
  </header>

  <main id="playground" class="layout">
    <section class="editor-panel">
      <div class="panel-header">
        <h2>Obligation</h2>
        <div class="controls">
          <label for="lang-select">Language:</label>
          <select id="lang-select">
            <option value="smtlib">SMT-LIB</option>
            <option value="lean">Lean</option>
            <option value="coq">Coq</option>
            <option value="idris2">Idris2</option>
            <option value="agda">Agda</option>
          </select>

          <label for="class-select">Class:</label>
          <select id="class-select">
            <option value="auto">auto (recommend)</option>
            <option value="safety">safety</option>
            <option value="linearity">linearity</option>
            <option value="termination">termination</option>
            <option value="equiv">equiv</option>
            <option value="correctness">correctness</option>
            <option value="confluence">confluence</option>
            <option value="totality">totality</option>
            <option value="invariant">invariant</option>
            <option value="refinement">refinement</option>
            <option value="model-check">model-check</option>
            <option value="other">other</option>
          </select>

          <label for="prover-select">Prover:</label>
          <select id="prover-select">
            <option value="auto">auto (strategy)</option>
            <option value="Z3">Z3</option>
            <option value="CVC5">CVC5</option>
            <option value="Coq">Coq</option>
            <option value="Lean">Lean</option>
            <option value="Idris2">Idris2</option>
            <option value="Agda">Agda</option>
            <option value="Isabelle">Isabelle</option>
            <option value="Dafny">Dafny</option>
            <option value="FStar">F*</option>
          </select>
        </div>
      </div>
      <div id="editor" class="editor" aria-label="Proof obligation editor"></div>
      <div class="actions">
        <button id="prove-btn" class="btn-primary">Prove</button>
        <button id="clear-btn" class="btn-secondary">Clear</button>
        <span id="status" class="status" role="status" aria-live="polite"></span>
      </div>
    </section>

    <section class="result-panel">
      <div class="panel-header">
        <h2>Result</h2>
      </div>
      <div id="result" class="result">
        <p class="placeholder">Submit an obligation to see the prover's verdict.</p>
      </div>
    </section>

    <aside class="strategy-panel">
      <div class="panel-header">
        <h2>Strategy</h2>
      </div>
      <div id="strategy" class="strategy">
        <p class="placeholder">Top provers by class will appear here once the learning loop is wired.</p>
      </div>
    </aside>
  </main>

  <footer class="site-footer">
    <p>
      <a href="https://github.com/hyperpolymath/nesy-solver">source</a> ·
      <a href="/about">about</a> ·
      <a href="https://nesy-solver.dev">nesy-solver.dev</a>
    </p>
    <p class="licence">MPL-2.0 © 2026 Jonathan D.A. Jewell (hyperpolymath)</p>
  </footer>

  <script type="module" src="/public/app.js"></script>
</body>
</html>