LeanDojoWebsite/leancopilot.html at main · lean-dojo/LeanDojoWebsite · 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
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
<!DOCTYPE html>
<html>
<head>
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean</title>

    <link rel="apple-touch-icon" sizes="180x180" href="/apple-touch-icon.png">
    <link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png">
    <link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png">
    <link rel="manifest" href="/site.webmanifest">
    <meta name="msapplication-TileColor" content="#da532c">
    <meta name="theme-color" content="#ffffff">

    <script src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
    <script id="MathJax-script" async src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>

    <link href="https://fonts.googleapis.com/css?family=Google+Sans|Noto+Sans|Castoro"
          rel="stylesheet">

    <link rel="stylesheet" href="./static/css/bulma.min.css">
    <link rel="stylesheet" href="./static/css/bulma-carousel.min.css">
    <link rel="stylesheet" href="./static/css/bulma-slider.min.css">
    <link rel="stylesheet" href="./static/css/fontawesome.all.min.css">
    <link rel="stylesheet" href="./static/css/academicons.min.css">
    <link rel="stylesheet"
          href="https://cdn.jsdelivr.net/gh/jpswalsh/academicons@1/css/academicons.min.css">
    <link rel="stylesheet" href="./static/css/index.css">

    <script src="https://ajax.googleapis.com/ajax/libs/jquery/3.5.1/jquery.min.js"></script>
    <script defer src="./static/js/fontawesome.all.min.js"></script>
    <script>
        document.addEventListener('DOMContentLoaded', () => {
            const $navbarBurgers = Array.prototype.slice.call(document.querySelectorAll('.navbar-burger'), 0);
            if ($navbarBurgers.length > 0) {
                $navbarBurgers.forEach(el => {
                    el.addEventListener('click', () => {
                        const target = el.dataset.target;
                        const $target = document.getElementById(target);
                        el.classList.toggle('is-active');
                        $target.classList.toggle('is-active');
                    });
                });
            }
        });
    </script>
</head>
<body>

<!-- Navigation -->
<nav class="navbar is-light" role="navigation" aria-label="main navigation">
    <div class="navbar-brand">
        <a class="navbar-item" href="index.html">
            <strong>LeanDojo</strong>
        </a>

        <a role="button" class="navbar-burger" aria-label="menu" aria-expanded="false" data-target="navbarBasicExample">
            <span aria-hidden="true"></span>
            <span aria-hidden="true"></span>
            <span aria-hidden="true"></span>
        </a>
    </div>

    <div id="navbarBasicExample" class="navbar-menu">
        <div class="navbar-start">
            <a class="navbar-item" href="index.html">
                Home
            </a>
            <a class="navbar-item" href="leandojo.html">
                LeanDojo
            </a>
            <a class="navbar-item" href="leanagent.html">
                LeanAgent
            </a>
            <a class="navbar-item is-active" href="leancopilot.html">
                LeanCopilot
            </a>
            <a class="navbar-item" href="leanprogress.html">
                LeanProgress
            </a>
            <a class="navbar-item" href="leanide.html">
                LeanIDE
            </a>
            <a class="navbar-item" href="torchlean.html">
                TorchLean
            </a>
            <a class="navbar-item" href="bridge.html">
                BRIDGE
            </a>
        </div>
    </div>
</nav>

<section class="hero">
    <div class="hero-body">
        <div class="container is-max-desktop">
            <div class="columns is-centered">
                <div class="column has-text-centered">
                    <h1 class="title is-1 publication-title">Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean</h1>
                    <div class="is-size-5 publication-authors">
                        <span class="author-block">
                            <a href="https://peiyang-song.github.io/">Peiyang Song</a> <a href="mailto:psong@caltech.edu"><i class="fas fa-envelope"></i></a><sup>1</sup>,</span>
                        <span class="author-block">
                            <a href="https://yangky11.github.io/">Kaiyu Yang</a><sup>1</sup>,</span>
                        <span class="author-block">
                            <a href="http://tensorlab.cms.caltech.edu/users/anima/">Anima Anandkumar</a><sup>1</sup></span>
                    </div>

                    <div class="is-size-5 publication-authors">
                        <span class="author-block"><sup>1</sup>California Institute of Technology</span>
                    </div>

                    <div class="is-size-5 publication-authors">
                        <span class="author-block"><strong>Published:</strong> International Conference on
Neuro-symbolic Systems (NeuS) 2025</span>
                    </div>

                    <div class="column has-text-centered">
                        <div class="publication-links">
                            <span class="link-block">
                                <a href="https://arxiv.org/abs/2404.12534" class="external-link button is-normal is-rounded is-dark">
                                <span class="icon">
                                    <i class="fas fa-file-pdf"></i>
                                </span>
                                <span>arXiv</span>
                                </a>
                            </span>
                            <span class="link-block">
                                <a target="_blank" href="https://github.com/lean-dojo/LeanCopilot"
                                class="external-link button is-normal is-rounded is-dark">
                                <span class="icon">
                                    <i class="fab fa-github"></i>
                                </span>
                                <span>Code</span>
                                </a>
                            </span>
                        </div>
                    </div>
                </div>
            </div>
        </div>
    </div>
</section>

<section class="section">
    <div class="container is-max-widescreen">
        <div class="rows">
            <div class="rows is-centered ">
                <div class="row is-full-width">
                    <h2 class="title is-3"><span class="lean-infer">Abstract</span></h2>
                    <p style="font-size: 125%">Lean Copilot addresses the grand challenge of human-AI collaboration in formal theorem proving by introducing large language models as intelligent assistants within the Lean proof environment. This system bridges the gap between human mathematical intuition and machine computational power, enabling seamless collaboration in formal proof development.</p>
                    <br />
                    <p style="font-size: 125%">The system provides real-time assistance through tactic suggestion, premise selection, and automated proof search, fundamentally transforming how mathematicians interact with formal proof systems and accelerating the formalization of mathematical knowledge.</p>
                    <br />
                    <video controls>
            		  <source src="images/Lean Copilot demo.mp4" type="video/mp4">
            		  Your browser does not support HTML video.
            		</video>
                </div>
            </div>
        </div>
    </div>
</section>

<section class="section">
    <div class="container is-max-widescreen">
        <div class="rows">
            <div class="rows is-centered">
                <div class="row is-full-width">
                    <h2 class="title is-3"><span class="dvima">Technical Architecture</span></h2>
                    <div class="content">
                        <p style="font-size: 125%">Lean Copilot implements a sophisticated human-in-the-loop architecture that seamlessly integrates large language models with the Lean theorem prover:</p>
                        <br />
                        <div class="columns">
                            <div class="column">
                                <h3 class="title is-4">Intelligent Tactic Suggestion</h3>
                                <p style="font-size: 125%">Context-aware tactic recommendations based on current proof state and mathematical context, leveraging deep understanding of Lean's tactic language and proof patterns.</p>
                            </div>
                            <div class="column">
                                <h3 class="title is-4">Dynamic Premise Selection</h3>
                                <p style="font-size: 125%">Automated identification and retrieval of relevant theorems and lemmas from Lean's extensive mathematical library using semantic similarity and logical relevance.</p>
                            </div>
                            <div class="column">
                                <h3 class="title is-4">Guided Proof Search</h3>
                                <p style="font-size: 125%">Advanced search algorithms that combine human guidance with automated exploration to discover complete proofs efficiently.</p>
                            </div>
                        </div>
                    </div>
                </div>
            </div>
        </div>
    </div>
</section>

<section class="section">
    <div class="container is-max-widescreen">
        <div class="rows">
            <div class="rows is-centered">
                <div class="row is-full-width">
                    <h2 class="title is-3"><span class="dvima">Human-AI Collaboration Paradigm</span></h2>
                    <div class="content">
                        <p style="font-size: 125%">Lean Copilot pioneered a new paradigm of human-AI collaboration in formal mathematics, where AI serves as an intelligent assistant rather than a replacement for human mathematical reasoning:</p>
                        <br />
                        <div class="columns">
                            <div class="column">
                                <h4 class="title is-5">Interactive Assistance</h4>
                                <p style="font-size: 125%">Real-time suggestions and guidance that adapt to the mathematician's proof strategy and style, maintaining human agency in the proof development process.</p>
                            </div>
                            <div class="column">
                                <h4 class="title is-5">Flexible Deployment</h4>
                                <p style="font-size: 125%">Support for local, cloud, and custom model deployment options, enabling researchers to choose the configuration that best fits their privacy and performance requirements.</p>
                            </div>
                            <div class="column">
                                <h4 class="title is-5">Extensible Framework</h4>
                                <p style="font-size: 125%">Modular architecture that allows integration of new models and techniques, fostering continued innovation in AI-assisted theorem proving.</p>
                            </div>
                        </div>
                    </div>
                </div>
            </div>
        </div>
    </div>
</section>

<section class="section">
    <div class="container is-max-widescreen">
        <div class="rows">
            <div class="rows is-centered">
                <div class="row is-full-width">
                    <h2 class="title is-3"><span class="dvima">Getting Started</span></h2>
                    <div class="content">
                        <p style="font-size: 125%">To get started with Lean Copilot, visit our <a target="_blank" href="https://github.com/lean-dojo/LeanCopilot">GitHub repository</a> for installation instructions and usage examples.</p>
                    </div>
                </div>
            </div>
        </div>
    </div>
</section>

<footer class="footer">
    <div class="container">
        <div class="columns is-centered">
            <div class="column">
                <div class="content has-text-centered">
                    <p>
                        Website template borrowed from <a
                            href="https://vimalabs.github.io/">VIMA</a>.
                    </p>
                </div>
            </div>
        </div>
    </div>
</footer>

</body>
</html>