-
Notifications
You must be signed in to change notification settings - Fork 59
Expand file tree
/
Copy pathindex.html
More file actions
294 lines (288 loc) · 24.7 KB
/
Copy pathindex.html
File metadata and controls
294 lines (288 loc) · 24.7 KB
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
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>MathCode — A Frontier Mathematical Coding Agent</title>
<meta name="description" content="MathCode is a terminal AI coding agent with a built-in math formalization engine: describe a problem in plain language and it converts it into a Lean 4 theorem and attempts a formal proof.">
<meta property="og:title" content="MathCode — A Frontier Mathematical Coding Agent"/>
<meta property="og:description" content="A terminal AI coding agent that formalizes math problems into Lean 4 theorems and proves them."/>
<meta property="og:type" content="website"/>
<meta property="og:url" content="https://math-ai-org.github.io/mathcode/"/>
<link rel="canonical" href="https://math-ai-org.github.io/mathcode/">
<link rel="icon" href="data:image/svg+xml,%3Csvg xmlns='http://www.w3.org/2000/svg' viewBox='0 0 100 100'%3E%3Crect width='100' height='100' rx='22' fill='%230A0A0A'/%3E%3Ctext x='50' y='55' font-family='Arial,sans-serif' font-size='40' font-weight='700' fill='white' text-anchor='middle' dominant-baseline='central'%3EMC%3C/text%3E%3C/svg%3E" type="image/svg+xml">
<link rel="preconnect" href="https://fonts.googleapis.com" />
<link rel="preconnect" href="https://fonts.gstatic.com" crossorigin />
<link href="https://fonts.googleapis.com/css2?family=Space+Grotesk:wght@400;500;600;700&family=Inter:wght@400;500;600;700&display=swap" rel="stylesheet" />
<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/6.5.2/css/all.min.css" />
<style>
/* ===== Monochrome system (OpenAI x SpaceX) — skins existing markup ===== */
:root{
--bg:#FFFFFF; --bg-subtle:#F7F7F5; --bg-subtle-2:#EFEFEC;
--ink:#0A0A0A; --ink-2:#3A3A3A; --ink-3:#6B6B6B; --line:#E7E7E3;
--d-bg:#0A0A0A; --d-ink:#FFFFFF; --d-ink-2:rgba(255,255,255,.62);
--d-ink-3:rgba(255,255,255,.42); --d-line:rgba(255,255,255,.14);
--nav-h:68px; --maxw:1120px; --readw:1120px; --ease:cubic-bezier(.22,.61,.36,1);
--primary-color:#0A0A0A; --accent-color:#0A0A0A; --content-bg:#F7F7F5;
--border-color:#E7E7E3; --text-main:#3A3A3A; --text-on-primary:#FFFFFF;
--link-color:#0A0A0A; --link-hover-color:#0A0A0A; --primary-color-rgb:10,10,10; --link-color-rgb:10,10,10;
}
*,*::before,*::after{box-sizing:border-box}
html{scroll-behavior:smooth;-webkit-text-size-adjust:100%}
body{margin:0;font-family:'Inter',system-ui,-apple-system,Segoe UI,Roboto,Arial,sans-serif;
background:var(--bg);color:var(--ink);line-height:1.6;overflow-x:hidden;display:flex;flex-direction:column;min-height:100vh;
text-rendering:optimizeLegibility;-webkit-font-smoothing:antialiased;-moz-osx-font-smoothing:grayscale}
a{color:inherit;text-decoration:none} img{max-width:100%;display:block} ::selection{background:var(--ink);color:var(--bg)}
body.nav-open{overflow:hidden}
.container{width:100%;max-width:var(--maxw);margin:0 auto;padding-inline:clamp(1.25rem,5vw,3rem)}
.section.content-section .container{max-width:var(--readw)}
.has-text-centered{text-align:center!important} .has-text-justified{text-align:justify}
.has-text-grey{color:var(--ink-3)!important} .is-italic{font-style:italic}
.has-text-weight-bold{font-weight:700} .has-text-weight-medium{font-weight:500}
.is-size-3{font-size:1.5rem} .is-size-4{font-size:1.3rem} .is-size-5{font-size:1.15rem} .is-size-6{font-size:1rem} .is-size-7{font-size:.82rem}
.mb-6{margin-bottom:1.5rem!important} .mt-3{margin-top:.75rem!important} .mt-5{margin-top:1.25rem!important} .mt-6{margin-top:2rem!important}
.my-4{margin-top:1rem!important;margin-bottom:1rem!important} .my-5{margin-top:1.5rem!important;margin-bottom:1.5rem!important}
.tight{margin-top:.5rem!important;margin-bottom:.75rem!important}
.icon{display:inline-flex;align-items:center;justify-content:center}
hr{border:0;border-top:1px solid var(--line);margin:1rem 0}
/* Nav */
.navbar{position:fixed;inset:0 0 auto 0;z-index:200;height:var(--nav-h);display:flex;align-items:center;background:transparent;
border-bottom:1px solid transparent;transition:background .4s var(--ease),border-color .4s var(--ease),backdrop-filter .4s var(--ease)}
.navbar>.container{display:flex;align-items:center;justify-content:space-between}
.navbar-brand{display:flex;align-items:center;position:relative;z-index:160;min-height:auto}
.navbar-brand .navbar-item{font-family:'Space Grotesk',sans-serif;font-weight:600;font-size:1.05rem;letter-spacing:.14em;
text-transform:uppercase;color:var(--d-ink);padding:0;background:transparent!important;transition:color .4s var(--ease)}
.navbar-menu{display:flex;box-shadow:none;background:transparent;padding:0} .navbar-end{display:flex;align-items:center;gap:1.8rem;margin-left:auto}
.navbar-menu .navbar-item{position:relative;font-size:.78rem;font-weight:600;letter-spacing:.12em;text-transform:uppercase;
color:var(--d-ink-2);padding:.25rem 0;background:transparent!important;transition:color .25s var(--ease)}
.navbar-menu .navbar-item::after{content:"";position:absolute;left:0;right:0;bottom:-4px;height:1px;background:currentColor;
transform:scaleX(0);transform-origin:left;transition:transform .3s var(--ease)}
.navbar-menu .navbar-item:hover{color:var(--d-ink)} .navbar-menu .navbar-item:hover::after{transform:scaleX(1)}
.navbar.is-scrolled{background:rgba(255,255,255,.82);backdrop-filter:saturate(180%) blur(20px);
-webkit-backdrop-filter:saturate(180%) blur(20px);border-bottom-color:var(--line)}
.navbar.is-scrolled .navbar-brand .navbar-item{color:var(--ink)}
.navbar.is-scrolled .navbar-menu .navbar-item{color:var(--ink-3)}
.navbar.is-scrolled .navbar-menu .navbar-item:hover{color:var(--ink)}
.navbar-burger{display:none;position:relative;width:44px;height:44px;margin:0;background:none;border:0;cursor:pointer}
.navbar-burger span{position:absolute;left:13px;width:18px;height:1.5px;background:var(--d-ink);
transition:transform .35s var(--ease),opacity .2s var(--ease),background .4s var(--ease)}
.navbar-burger span:nth-child(1){top:18px} .navbar-burger span:nth-child(2){top:23px} .navbar-burger span:nth-child(3){top:28px}
.navbar.is-scrolled .navbar-burger span{background:var(--ink)}
.navbar-burger.is-active span{background:var(--d-ink)!important}
.navbar-burger.is-active span:nth-child(1){top:23px;transform:rotate(45deg)}
.navbar-burger.is-active span:nth-child(2){opacity:0}
.navbar-burger.is-active span:nth-child(3){top:23px;transform:rotate(-45deg)}
/* Hero */
.hero{position:relative;background:var(--d-bg);color:var(--d-ink);overflow:hidden;padding-top:var(--nav-h);
min-height:62vh;min-height:62svh;display:flex;align-items:center}
.hero::before{content:"";position:absolute;inset:0;
background-image:linear-gradient(to right,rgba(255,255,255,.045) 1px,transparent 1px),linear-gradient(to bottom,rgba(255,255,255,.045) 1px,transparent 1px);
background-size:64px 64px;-webkit-mask-image:radial-gradient(ellipse 85% 75% at 50% 40%,#000 25%,transparent 78%);
mask-image:radial-gradient(ellipse 85% 75% at 50% 40%,#000 25%,transparent 78%)}
.hero::after{content:"";position:absolute;left:50%;top:38%;transform:translate(-50%,-50%);width:80vw;height:80vw;
max-width:1000px;max-height:1000px;background:radial-gradient(circle,rgba(255,255,255,.11),transparent 62%);pointer-events:none}
.hero-body{position:relative;z-index:1;width:100%;padding-block:clamp(2.5rem,7vh,4.5rem)}
.hero .title{font-family:'Space Grotesk',sans-serif;font-weight:500;letter-spacing:-.035em;line-height:1.02;
color:var(--d-ink);font-size:clamp(2.4rem,6vw,4.6rem);margin-bottom:0}
.hero .subtitle{color:var(--d-ink-2)}
.hero .subtitle.is-hero-subtitle{color:var(--d-ink-2);font-size:clamp(1.05rem,1.7vw,1.35rem);max-width:820px;margin:1.2rem auto 0;font-weight:400;line-height:1.55}
.hero .subtitle .highlight{color:var(--d-ink);font-weight:500}
.hero .subtitle.is-4,.hero .subtitle.is-5{font-size:1.05rem;font-weight:500;margin-top:1.2rem;line-height:1.55}
.hero .subtitle.is-6{font-size:.85rem;margin-top:.4rem}
.hero .subtitle a,.authors-list a{color:var(--d-ink);border-bottom:1px solid var(--d-line)}
.hero .subtitle a:hover,.authors-list a:hover{border-bottom-color:var(--d-ink)}
.authors-list{font-size:1.02rem;line-height:1.7;margin-top:1.6rem;color:var(--d-ink-2);font-weight:500}
.affiliations{font-size:.78rem;letter-spacing:.16em;text-transform:uppercase;color:var(--d-ink-3);margin-top:.7rem}
.project-links{margin-top:1.6rem}
.project-links a{color:var(--d-ink-2);font-size:1.2rem;margin:0 .55rem;transition:color .2s var(--ease),transform .2s var(--ease)}
.project-links a:hover{color:var(--d-ink);transform:translateY(-2px)}
.pill{display:inline-block;padding:.4rem .85rem;border-radius:100px;font-size:.68rem;font-weight:600;letter-spacing:.1em;
text-transform:uppercase;background:transparent;color:var(--d-ink-2);border:1px solid var(--d-line);margin:.22rem .2rem}
/* Sections / body */
.section.content-section{padding-block:clamp(3.5rem,8vh,6rem);border-bottom:1px solid var(--line)}
.section.content-section:nth-child(even){background:var(--bg-subtle)}
.section.content-section:last-of-type{border-bottom:none}
.section-title,.title.is-3.section-title{font-family:'Space Grotesk',sans-serif;font-weight:600;letter-spacing:-.03em;line-height:1.1;
color:var(--ink);font-size:clamp(1.7rem,3.6vw,2.3rem);margin-bottom:1.75rem!important;text-align:left!important}
.content{max-width:var(--readw);margin:0 auto;line-height:1.8;font-size:1.06rem;color:var(--ink-2)}
.content .title.is-4,.title.is-4,.content h3{font-family:'Space Grotesk',sans-serif;font-weight:600;letter-spacing:-.02em;color:var(--ink);font-size:1.3rem;margin:2.1rem 0 1rem}
.content .title.is-5,.title.is-5,.content h4{font-family:'Space Grotesk',sans-serif;font-weight:600;color:var(--ink);font-size:1.12rem;margin:1.6rem 0 .6rem;line-height:1.3}
.content p{margin-bottom:1.2rem;color:var(--ink-2)} .content strong{color:var(--ink);font-weight:600}
.content a{color:var(--ink);border-bottom:1px solid var(--ink-3);font-weight:500;transition:border-color .2s var(--ease)}
.content a:hover{border-bottom-color:var(--ink)}
.content ul,.content ol{margin:0 0 1.2rem 1.4rem} .content li{margin-bottom:.5rem;color:var(--ink-2)}
.content img{display:block;margin:1.75rem auto;max-width:100%;border:1px solid var(--line);border-radius:12px}
.content figure{margin:1.75rem auto;text-align:center;max-width:100%}
.content figure img,figure img{margin:0 auto .6rem}
figcaption,.content figcaption{color:var(--ink-3);font-size:.85rem;line-height:1.6;max-width:820px;margin:.4rem auto 0}
.math-block{margin:1.6rem 0;overflow-x:auto;text-align:center}
.content pre,pre{background:var(--d-bg);color:#E7E7E3;border:1px solid var(--line);border-radius:12px;padding:1.2em 1.3em;overflow:auto;font-size:.9rem;margin:1.4rem 0;line-height:1.65}
code{background:var(--bg-subtle-2);color:var(--ink);padding:.16em .4em;border-radius:5px;font-size:85%}
pre code{background:transparent;color:inherit;padding:0;font-size:inherit}
.notification{position:relative;background:var(--bg-subtle);border-radius:0 10px 10px 0;padding:1.1rem 1.4rem;margin:1.6rem 0;color:var(--ink-2)}
.message{background:var(--bg-subtle);border-left:2px solid var(--ink);border-radius:0 10px 10px 0;margin:1.6rem 0}
.message-body{padding:1.1rem 1.4rem;color:var(--ink-2);border:0}
.box{background:var(--bg);border:1px solid var(--line);border-radius:12px;padding:1.5rem;margin:1rem 0;box-shadow:none;color:var(--ink-2)}
.has-background-light{background:var(--bg-subtle)!important}
.pillar-box,.book-item{background:var(--bg);border:1px solid var(--line);border-radius:12px;padding:1.25rem;height:100%;color:var(--ink-2);transition:transform .2s var(--ease),box-shadow .2s var(--ease)}
.book-item{font-size:.92rem;text-align:center}
.pillar-box:hover,.book-item:hover{transform:translateY(-3px);box-shadow:0 12px 28px rgba(10,10,10,.06)}
.section.content-section:nth-child(even) :is(.notification,.message,.box,.pillar-box,.book-item,.diagram-container){background:#fff}
.columns{display:flex;flex-wrap:wrap;gap:1.5rem;margin:1rem 0} .columns.is-centered{justify-content:center} .columns.is-vcentered{align-items:center}
.column{flex:1 1 0;min-width:0;padding:0}
.column.is-4{flex:0 0 calc(33.333% - 1rem)} .column.is-5{flex:0 0 calc(41.666% - .75rem)}
.column.is-6,.column.is-half{flex:0 0 calc(50% - .75rem)} .column.is-one-quarter-desktop{flex:0 0 calc(25% - 1.125rem)}
.table-container{overflow-x:auto;margin:2rem 0;border:1px solid var(--line);border-radius:12px}
table.table,.table{width:100%;border-collapse:collapse;background:var(--bg);margin:0}
table.table th,.table th{background:var(--bg-subtle);color:var(--ink);font-weight:600;padding:1rem;text-align:left;border-bottom:2px solid var(--line)}
table.table td,.table td{padding:1rem;border-bottom:1px solid var(--line);color:var(--ink-2);vertical-align:top}
table.table tr:last-child td{border-bottom:none}
.diagram-container{width:100%;margin:2rem 0;text-align:center;background:var(--bg);border:1px solid var(--line);border-radius:12px;padding:1.5rem;display:block}
.diagram-container img{border:0;margin:0 auto}
.mini-caption{display:block;margin-top:.6rem;color:var(--ink-3);font-style:italic;font-size:.85rem;text-align:center}
.profile-image{width:100%;max-width:280px;aspect-ratio:1;object-fit:cover;border-radius:14px;border:1px solid var(--line);filter:grayscale(1)}
svg text{font-family:'Inter',sans-serif}
.button{display:inline-flex;align-items:center;gap:.5rem;padding:.6rem 1.1rem;border:1px solid var(--ink);border-radius:100px;
background:transparent;color:var(--ink);font-family:inherit;font-size:.72rem;font-weight:600;letter-spacing:.12em;text-transform:uppercase;
cursor:pointer;transition:background .2s var(--ease),color .2s var(--ease);margin:.25rem}
.button:hover,.button.is-primary,.button.is-success{background:var(--ink);color:var(--bg)!important;border-color:var(--ink)}
/* Footer */
.footer{background:var(--d-bg);color:var(--d-ink-2);padding-block:clamp(2.5rem,5vw,4rem);margin-top:auto;border-top:1px solid var(--d-line)}
.footer .content{max-width:var(--maxw);color:var(--d-ink-2)}
.footer .content p:first-child{font-size:.78rem;font-weight:600;letter-spacing:.1em;text-transform:uppercase;margin-bottom:1rem;line-height:2.1}
.footer a{color:var(--d-ink-2);font-weight:600;transition:color .2s var(--ease)} .footer a:hover{color:var(--d-ink)}
.footer .content p:last-child{font-size:.85rem;color:var(--d-ink-3);letter-spacing:0;text-transform:none;font-weight:400}
@media(max-width:1023px){ .column.is-half-tablet,.column.is-one-quarter-desktop{flex:0 0 calc(50% - .75rem)} }
@media(max-width:820px){
.navbar-burger{display:block}
.navbar-menu{position:fixed;inset:0;background:var(--d-bg);flex-direction:column;justify-content:center;align-items:center;gap:1.5rem;
opacity:0;visibility:hidden;transform:translateY(-8px);z-index:150;transition:opacity .4s var(--ease),transform .4s var(--ease),visibility .4s}
.navbar-menu.is-active{opacity:1;visibility:visible;transform:none}
.navbar-end{flex-direction:column;gap:1.5rem;margin-left:0}
.navbar-menu .navbar-item{font-family:'Space Grotesk',sans-serif;font-size:1.4rem;font-weight:500;letter-spacing:-.01em;text-transform:none}
.navbar-menu .navbar-item::after{display:none}
.column,.column.is-4,.column.is-5,.column.is-6,.column.is-half,.column.is-half-tablet,.column.is-one-quarter-desktop{flex:1 1 100%}
}
@media (prefers-reduced-motion: reduce){ html{scroll-behavior:auto} }
</style>
</head>
<body>
<nav class="navbar" role="navigation" aria-label="main navigation">
<div class="container">
<div class="navbar-brand">
<a class="navbar-item" href="#">MathCode</a>
<a role="button" class="navbar-burger" aria-label="menu" aria-expanded="false" data-target="navbarMenu"><span aria-hidden="true"></span><span aria-hidden="true"></span><span aria-hidden="true"></span></a>
</div>
<div id="navbarMenu" class="navbar-menu"><div class="navbar-end">
<a href="#overview" class="navbar-item">Overview</a>
<a href="#quickstart" class="navbar-item">Quick Start</a>
<a href="#features" class="navbar-item">Features</a>
<a href="#citation" class="navbar-item">Citation</a>
<a href="https://yfz.ai/blog" class="navbar-item">Blog</a>
</div></div>
</div>
</nav>
<header class="hero is-medium">
<div class="hero-body"><div class="container has-text-centered">
<h1 class="title">MathCode</h1>
<h2 class="subtitle is-hero-subtitle"><span class="highlight">A Frontier Mathematical Coding Agent</span><br>A terminal AI coding assistant with a built-in math formalization engine — describe a problem in plain language and it converts it into a Lean 4 theorem and attempts a formal proof.</h2>
<div class="project-links">
<a href="https://github.com/math-ai-org/mathcode" target="_blank" rel="noopener" aria-label="GitHub"><i class="fab fa-github"></i></a>
<a href="https://discord.gg/f2AFP9W5" target="_blank" rel="noopener" aria-label="Discord"><i class="fab fa-discord"></i></a>
<a href="#citation" aria-label="Citation"><i class="fas fa-quote-right"></i></a>
</div>
<div style="margin-top:1.25rem;">
<span class="pill">Lean 4</span><span class="pill">Formal Proof</span><span class="pill">AI Agent</span><span class="pill">Mathlib</span>
</div>
</div></div>
</header>
<main>
<section id="overview" class="section content-section"><div class="container">
<h2 class="section-title">Overview</h2>
<div class="content">
<p>MathCode is a terminal AI coding assistant with a built-in math formalization engine. Give it a math problem in plain language and it will automatically convert it into a <strong>Lean 4</strong> theorem and attempt a formal proof — with a persistent Lean REPL, reusable theorem and axiom libraries, agentic proving, and an Obsidian knowledge graph.</p>
<figure><img src="Demo.png" alt="MathCode demo"></figure>
</div>
</div></section>
<section id="quickstart" class="section content-section"><div class="container">
<h2 class="section-title">Quick Start</h2>
<div class="content">
<p>Requires macOS (arm64) or Linux (x86_64), plus the <code>codex</code> CLI for the default backend.</p>
<pre><code>git clone https://github.com/math-ai-org/mathcode.git
cd mathcode
bash setup.sh
codex auth login
mathcode</code></pre>
<p><code>setup.sh</code> prepares the release checkout, downloads the bundled runtime and Lean toolchain, and installs a user-local <code>mathcode</code> launcher. Try it with:</p>
<pre><code>mathcode -p "prove that the square of an even number is even"</code></pre>
<p>Outputs are written to <code>LeanFormalizations/</code>. A browser UI is available via <code>./run webui</code>.</p>
</div>
</div></section>
<section id="features" class="section content-section"><div class="container">
<h2 class="section-title">Features</h2>
<div class="columns is-multiline">
<div class="column is-4"><div class="pillar-box"><strong>Persistent Lean REPL</strong><p style="margin:.5rem 0 0">A persistent Lean language server brings compile checks to <strong>~0.4s</strong> after a one-time warmup, instead of ~30s.</p></div></div>
<div class="column is-4"><div class="pillar-box"><strong>Theorem Library</strong><p style="margin:.5rem 0 0">Every proved theorem is auto-named, stored, and made importable so the prover and planner can reuse it.</p></div></div>
<div class="column is-4"><div class="pillar-box"><strong>Axiom Library</strong><p style="margin:.5rem 0 0">Store conversational assumptions as persistent, compile-checked, consistency-reviewed Lean declarations.</p></div></div>
<div class="column is-4"><div class="pillar-box"><strong>Lean LSP Integration</strong><p style="margin:.5rem 0 0">Searches leansearch.net and Loogle for verified Mathlib lemmas and uses structured LSP diagnostics for repairs.</p></div></div>
<div class="column is-4"><div class="pillar-box"><strong>Obsidian Theorem Graph</strong><p style="margin:.5rem 0 0">Generates an Obsidian vault that visualizes theorem-to-lemma dependencies as a knowledge graph.</p></div></div>
<div class="column is-4"><div class="pillar-box"><strong>Agent-Mode Proving</strong><p style="margin:.5rem 0 0">Each proof becomes an interactive session where the agent writes candidates, reads errors, and recompiles.</p></div></div>
<div class="column is-4"><div class="pillar-box"><strong>Tree-of-Subgoals</strong><p style="margin:.5rem 0 0">Decomposes complex theorems into independent subgoals and proves them in parallel, then stitches them back.</p></div></div>
<div class="column is-4"><div class="pillar-box"><strong>Multi-Planner</strong><p style="margin:.5rem 0 0">Runs multiple planners in parallel for diverse proof strategies; the prover picks the best approach.</p></div></div>
</div>
</div></section>
<section id="citation" class="section content-section"><div class="container">
<h2 class="section-title">Citation</h2>
<div class="content"><p>If you use MathCode in research, please cite:</p>
<pre id="cite-bibtex"><code>@misc{mathcode2026,
title = {MathCode: A Frontier Mathematical Coding Agent},
author = {Team Math-AI},
journal = {math-ai-org.github.io},
year = {2026},
month = {April},
url = {https://github.com/math-ai-org/mathcode}
}</code></pre>
<p><button id="copy-cite" class="button"><span class="icon"><i class="fas fa-clipboard"></i></span><span>Copy BibTeX</span></button></p>
<p>The math formalization and proving pipeline is based on the <a href="https://github.com/T3S1AMAX/autolean.git" target="_blank" rel="noopener">AUTOLEAN</a> project.</p></div>
</div></section>
</main>
<footer class="footer"><div class="container"><div class="content has-text-centered">
<p><a href="#overview">Overview</a> • <a href="#quickstart">Quick Start</a> •
<a href="#features">Features</a> • <a href="#citation">Citation</a> •
<a href="https://github.com/math-ai-org/mathcode">GitHub</a> •
<a href="https://discord.gg/f2AFP9W5">Discord</a> •
<a href="https://yfz.ai/blog">Yifan's Blog</a></p>
<p>© 2026 Team Math-AI.</p>
</div></div></footer>
<script>
document.addEventListener('DOMContentLoaded', () => {
const navbar = document.querySelector('.navbar');
const hero = document.querySelector('.hero');
const burgers = Array.from(document.querySelectorAll('.navbar-burger'));
if (navbar && hero && 'IntersectionObserver' in window) {
new IntersectionObserver(([e]) => navbar.classList.toggle('is-scrolled', !e.isIntersecting),
{ rootMargin: '-69px 0px 0px 0px', threshold: 0 }).observe(hero);
}
const closeMenu = () => {
document.querySelectorAll('.navbar-burger.is-active').forEach(b => b.classList.remove('is-active'));
document.querySelectorAll('.navbar-menu.is-active').forEach(m => m.classList.remove('is-active'));
document.body.classList.remove('nav-open');
};
burgers.forEach(el => el.addEventListener('click', () => {
const target = document.getElementById(el.dataset.target);
el.classList.toggle('is-active'); if (target) target.classList.toggle('is-active');
document.body.classList.toggle('nav-open', el.classList.contains('is-active'));
}));
document.querySelectorAll('.navbar-menu .navbar-item').forEach(a => a.addEventListener('click', closeMenu));
document.addEventListener('keydown', (e) => { if (e.key === 'Escape') closeMenu(); });
const btn = document.getElementById('copy-cite'), pre = document.getElementById('cite-bibtex');
if (btn && pre) { btn.addEventListener('click', async () => {
try { await navigator.clipboard.writeText(pre.innerText); btn.classList.add('is-success');
btn.innerHTML = '<span class="icon"><i class="fas fa-check"></i></span><span>Copied</span>';
setTimeout(() => { btn.classList.remove('is-success'); btn.innerHTML = '<span class="icon"><i class="fas fa-clipboard"></i></span><span>Copy BibTeX</span>'; }, 1600);
} catch (e) { const r=document.createRange(); r.selectNode(pre); const s=window.getSelection(); s.removeAllRanges(); s.addRange(r); try{document.execCommand('copy')}catch(_){}; s.removeAllRanges(); }
}); }
});
</script>
</body>
</html>