PageSourceSearch

https://lean-lang.org/fro/about/

html lean-lang.org collected 2026-09-24 08:55:10 UTC 141,513 bytes, 4,126 lines download raw bytes

1<!DOCTYPE html>
2<html lang="en">
3  <head>
4    <meta charset="UTF-8">
5    <base href="../.././"><style>:root {
6    /** Typography **/
7    /* The font family used for headers, ToC entries, etc */
8    --verso-structure-font-family: "Helvetica Neue", "Segoe UI", "Roboto", Arial, sans-serif;
9    /* The font family used for body text */
10    --verso-text-font-family: "Helvetica Neue", "Segoe UI", "Roboto", Arial, sans-serif;
11    /* The font family used for code */
12    --verso-code-font-family: monospace;
13
14    /** Text colors **/
15    --verso-text-color: black;
16    --verso-code-color: black;
17    --verso-structure-color: black;
18
19    /** Selected items (e.g. search results) */
20    --verso-selected-color: #def;
21
22    /** Tooltips **/
23    /*
24    These colors are used for the tooltips that display documentation and messages for code,
25    and for the equivalent popups that are shown when scripts are unavailable. The
26    severity-specific tooltip colors below default to the foreground and background given
27    here. The separator color draws the rule between sections of a tooltip's content.
28    */
29    --verso-tooltip-color: black;
30    --verso-tooltip-bg-color: #e5e5e5;
31    --verso-tooltip-border-color: black;
32    --verso-tooltip-separator-color: #ccc;
33
34    /** Message colors **/
35    /*
36    These colors are used to render Lean's feedback. Each severity (info, warning, error)
37    has four sets of related styles:
38
39    - The affected code itself: foreground and background, both at rest and while hovered,
40      plus the indicator color, which draws the wavy underline marking that a message is
41      present.
42    - The text of the message, via the message color.
43    - The tooltip that displays the message: foreground, background, and border. The border
44      color also draws the accent bar next to a message when it is shown without scripts,
45      and the background also colors the tooltip's arrow.
46    - The marker bar in the margin of output blocks, via the output color.
47    */
48    --verso-code-info-color: currentcolor;
49    --verso-code-info-bg-color: transparent;
50    --verso-code-info-hover-color: currentcolor;
51    --verso-code-info-hover-bg-color: #4777ff;
52    --verso-info-indicator-color: #4777ff;
53    --verso-message-info-color: black;
54    --verso-tooltip-info-color: var(--verso-tooltip-color);
55    --verso-tooltip-info-bg-color: var(--verso-tooltip-bg-color);
56    --verso-tooltip-info-border-color: #4777ff;
57    --verso-output-info-color: var(--verso-info-indicator-color);
58
59    --verso-code-warning-color: currentcolor;
60    --verso-code-warning-bg-color: transparent;
61    --verso-code-warning-hover-color: currentcolor;
62    --verso-code-warning-hover-bg-color: #ffd580;
63    --verso-warning-indicator-color: #e7a71d; /* 2.11 contrast ratio for white, 9.94 for black */
64    --verso-message-warning-color: black;
65    --verso-tooltip-warning-color: var(--verso-tooltip-color);
66    --verso-tooltip-warning-bg-color: var(--verso-tooltip-bg-color);
67    --verso-tooltip-warning-border-color: #ffd580;
68    --verso-output-warning-color: var(--verso-warning-indicator-color);
69
70    --verso-code-error-color: currentcolor;
71    --verso-code-error-bg-color: transparent;
72    --verso-code-error-hover-color: currentcolor;
73    --verso-code-error-hover-bg-color: #ffb3b3;
74    --verso-error-indicator-color: #ff0000;
75    --verso-message-error-color: #cc0000;
76    --verso-tooltip-error-color: var(--verso-tooltip-color);
77    --verso-tooltip-error-bg-color: var(--verso-tooltip-bg-color);
78    --verso-tooltip-error-border-color: #ffb3b3;
79    --verso-output-error-color: var(--verso-error-indicator-color);
80
81    /** Proof states **/
82    /*
83    These colors are used for the proof state displays that can be expanded inside of proofs
84    and shown in tooltips. The toggle colors are used for the control that expands and
85    collapses a proof state.
86    */
87    --verso-tactic-state-color: black;
88    --verso-tactic-state-bg-color: white;
89    --verso-tactic-state-border-color: #888888;
90    --verso-tactic-toggle-color: #bbbbbb;
91    --verso-tactic-toggle-checked-color: #999999;
92
93    /** Code Highlighting **/
94    /*
95    These variables control the rendering of Lean code emitted by Verso. Each category that can be
96    highlighted supports the customization of color, weight, style, and family.
97    */
98    /* Constants (e.g. `List` or `id` or `none`) */
99    --verso-code-const-color: var(--verso-code-color);
100    --verso-code-const-weight: normal;
101    --verso-code-const-style: normal;
102    --verso-code-const-font-family: var(--verso-code-font-family);
103
104    /* Keywords/atoms (e.g. `for` or `def` or `induction`) */
105    --verso-code-keyword-color: var(--verso-code-color);
106    --verso-code-keyword-weight: bold;
107    --verso-code-keyword-style: normal;
108    --verso-code-keyword-font-family: var(--verso-code-font-family);
109
110    /* Local bindings (e.g. `x` in `let x := 5`) */
111    --verso-code-var-color: var(--verso-code-color);
112    --verso-code-var-weight: normal;
113    --verso-code-var-style: italic;
114    --verso-code-var-font-family: var(--verso-code-font-family);
115
116    /* The background of interactive code while hovered (hoverable tokens, occurrences of a
117       hovered binding, and the tactics that expand to a proof state) */
118    --verso-code-hover-bg-color: #eeeeee;
119}
120</style><style>
121
122
123.hl.lean {
124  white-space: pre;
125  font-weight: normal;
126  font-style: normal;
127  font-size: inherit;
128}
129
130.hl.lean .keyword {
131  color: var(--verso-code-keyword-color,);
132  font-weight: var(--verso-code-keyword-weight, bold);
133  font-style: var(--verso-code-keyword-style, normal);
134  font-family: var(--verso-code-keyword-font-family,);
135}
136
137.hl.lean .const {
138  color: var(--verso-code-const-color,);
139  font-weight: var(--verso-code-const-weight, normal);
140  font-style: var(--verso-code-const-style, normal);
141  font-family: var(--verso-code-const-font-family,);
142}
143
144.hl.lean .var {
145  color: var(--verso-code-var-color,);
146  font-weight: var(--verso-code-var-weight, normal);
147  font-style: var(--verso-code-var-style, italic);
148  font-family: var(--verso-code-var-font-family,);
149
150  position: relative;
151}
152
153.hl.lean .literal, .hl.lean .unknown {
154  color: var(--verso-code-color,);
155  font-weight: normal;
156  font-style: normal;
157  font-family: var(--verso-code-font-family,);
158}
159
160/* These lexically-classified token kinds default to the `.unknown` appearance. The rule follows
161   `.const` so it wins for the `anon-ctor` tokens, which also carry the `const` class. */
162.hl.lean .anon-ctor,
163.hl.lean .number,
164.hl.lean .char,
165.hl.lean .comment,
166.hl.lean .punctuation,
167.hl.lean .delim,
168.hl.lean .wildcard {
169  color: var(--verso-code-color,);
170  font-weight: normal;
171  font-style: normal;
172  font-family: var(--verso-code-font-family,);
173}
174
175.hover-container {
176  width: 0;
177  height: 0;
178  position: relative;
179  display: inline;
180}
181
182.hl.lean a {
183  color: inherit;
184  text-decoration: currentcolor underline dotted;
185}
186
187.hl.lean a:hover {
188  text-decoration: currentcolor underline solid;
189}
190
191/* Links inside tooltips show their underline only when hovered. */
192.tippy-box .hl.lean a {
193  text-decoration: none;
194}
195
196.hl.lean .hover-info {
197  white-space: normal;
198}
199
200.hl.lean .token .hover-info {
201  display: none;
202  position: absolute;
203  color: var(--verso-tooltip-color, black);
204  background-color: var(--verso-tooltip-bg-color, #e5e5e5);
205  border: 1px solid var(--verso-tooltip-border-color, black);
206  padding: 0.5rem;
207  z-index: 300;
208}
209
210.hl.lean .hover-info.messages {
211  max-height: 10rem;
212  overflow-y: auto;
213  overflow-x: hidden;
214  scrollbar-gutter: stable;
215  padding: 0 0.5rem 0 0;
216  display: block;
217}
218
219.hl.lean .hover-info code {
220  white-space: pre-wrap;
221  background: none;
222}
223
224.hl.lean .hover-info code:not(.verso-message) {
225  color: var(--verso-tooltip-color, black);
226}
227
228.hl.lean .hover-info.messages > code {
229  padding: 0.5rem;
230  display: block;
231  width: fit-content;
232}
233
234.hl.lean .hover-info.messages > code:only-child {
235  margin: 0;
236}
237
238.hl.lean .hover-info.messages > code {
239  margin: 0.1rem;
240}
241
242.hl.lean .hover-info.messages > code:not(:first-child) {
243  margin-top: 0rem;
244}
245
246.hl.lean {
247}
248
249.hl.lean.block {
250  display: block;
251}
252
253.hl.lean.inline {
254  display: inline;
255  white-space: pre-wrap;
256}
257
258.hl.lean * {
259}
260
261.hl.lean .token {
262  transition: all 0.25s; /* Slight fade for highlights */
263}
264
265@media (hover: hover) {
266  /* Hovered content nested in a collapsed tactic region keeps its plain background: the
267     region's proof state is the tooltip that appears there, and its label is what
268     highlights. `:where` keeps the exclusion out of the specificity computation. */
269  .hl.lean .token.binding-hl,
270  .hl.lean :is(.literal, .token.typed, .token[data-verso-hover]):hover:not(:where(.tactic:has(> .tactic-toggle:not(:checked)) > label *)) {
271    background-color: var(--verso-code-hover-bg-color, #eeeeee);
272    border-radius: 2px;
273    transition: none;
274  }
275
276  /* Within a hovered message span, token hover backgrounds are removed so the span's own
277     hover background shows across the whole span. The exception is a hovered documented
278     token, which keeps its background because its tooltip is the one shown. */
279  .hl.lean .has-info:hover .token.binding-hl:not(:hover),
280  .hl.lean .has-info:hover .token.binding-hl:not([data-verso-hover]),
281  .hl.lean .has-info:hover .literal:hover:not([data-verso-hover]),
282  .hl.lean .has-info:hover .token.typed:hover:not([data-verso-hover]) {
283    background-color: transparent;
284  }
285}
286
287
288.hl.lean .has-info .token:not(.tactic-state):not(.tactic-state *), .hl.lean .has-info .inter-text:not(.tactic-state):not(.tactic-state *) {
289  text-decoration-style: wavy;
290  text-decoration-line: underline;
291  text-decoration-thickness: from-font;
292  text-decoration-skip-ink: none;
293}
294
295/*
296The underline color comes from the nearest enclosing message span: each severity's span rule
297sets `--verso--region-indicator-color`, which inherits, so a region nested inside one of
298another severity keeps its own indicator color.
299*/
300.hl.lean .has-info :not(.tactic-state):not(.tactic-state *) {
301  text-decoration-color: var(--verso--region-indicator-color);
302}
303
304.hl.lean .has-info .hover-info {
305  display: none;
306  position: absolute;
307  transform: translate(0.25rem, 0.3rem);
308  color: var(--verso-tooltip-color, black);
309  border: 1px solid var(--verso-tooltip-border-color, black);
310  padding: 0.5rem;
311  z-index: 400;
312  text-align: left;
313}
314
315.hl.lean .has-info.error {
316  --verso--region-indicator-color: var(--verso-error-indicator-color, #ff0000);
317  --verso--region-hover-color: var(--verso-code-error-hover-color, currentcolor);
318  --verso--region-hover-bg-color: var(--verso-code-error-hover-bg-color, #ffb3b3);
319  color: var(--verso-code-error-color, currentcolor);
320  background-color: var(--verso-code-error-bg-color, transparent);
321}
322
323/*
324The hover highlight follows the tooltip: a message span highlights only when its own tooltip
325is the one that appears. When a hovered nested message span, a hovered documented token, or
326a hovered collapsed tactic label shows its own tooltip instead, the message span does not
327highlight. A span nested in a collapsed tactic region likewise stays plain, because hovering
328it shows the region's proof state; `:where` keeps that exclusion out of the specificity
329computation.
330
331The hover colors come from `--verso--region-hover-color` and `--verso--region-hover-bg-color`,
332which each severity's span rule sets. This keeps the hover conditions in this one rule, and
333because the properties inherit, a region nested inside one of another severity keeps its own
334hover colors.
335*/
336@media (hover: hover) {
337  .hl.lean .has-info:hover:not(:has(.has-info:hover)):not(:has([data-verso-hover]:hover)):not(:has(.tactic > label:hover + .tactic-toggle:not(:checked))):not(:where(.tactic:has(> .tactic-toggle:not(:checked)) > label *)) {
338    color: var(--verso--region-hover-color, currentcolor);
339    background-color: var(--verso--region-hover-bg-color, transparent);
340  }
341}
342
343.hl.lean .hover-info.messages > code.error {
344  background-color: var(--verso-tooltip-error-bg-color, #e5e5e5);
345  border-left: 0.2rem solid var(--verso-tooltip-error-border-color, #ffb3b3);
346}
347
348/*
349A tooltip that shows only messages of the box's own severity leaves severity styling to the
350box itself. When messages of several severities share the tooltip, or a `mixed` tooltip
351combines messages with other content (such as documentation), each message keeps its
352severity accent to distinguish them.
353*/
354.tippy-box .hl.lean.mixed > .hover-info.messages {
355  margin-bottom: 0.5rem;
356}
357
358.tippy-box[data-theme~='error'] .hl.lean:not(.mixed) .hover-info.messages:not(:has(> code.warning)):not(:has(> code.information)) > code.error {
359  background: none;
360  border: none;
361}
362
363.error .verso-message, .error .verso-message .token, .error .verso-message label {
364  color: var(--verso-message-error-color, #cc0000);
365}
366
367.error .verso-message .case-label:has(input[type="checkbox"])::before {
368  background-color: var(--verso-message-error-color, #cc0000) !important;
369}
370
371.hl.lean .has-info.warning {
372  --verso--region-indicator-color: var(--verso-warning-indicator-color, #e7a71d);
373  --verso--region-hover-color: var(--verso-code-warning-hover-color, currentcolor);
374  --verso--region-hover-bg-color: var(--verso-code-warning-hover-bg-color, #ffd580);
375  color: var(--verso-code-warning-color, currentcolor);
376  background-color: var(--verso-code-warning-bg-color, transparent);
377}
378
379.hl.lean .hover-info.messages > code.warning {
380  background-color: var(--verso-tooltip-warning-bg-color, #e5e5e5);
381  border-left: 0.2rem solid var(--verso-tooltip-warning-border-color, #ffd580);
382}
383
384.lean-output {
385  border-left: 0.2em solid transparent;
386  padding: 0 0 0 0.5em;
387  border-top-left-radius: 0;
388  border-bottom-left-radius: 0;
389}
390
391.lean-output.error {
392  border-color: var(--verso-output-error-color, var(--verso-error-indicator-color, #ff0000));
393}
394
395.lean-output.information {
396  border-color: var(--verso-output-info-color, var(--verso-info-indicator-color, #4777ff));
397}
398
399.lean-output.warning {
400  border-color: var(--verso-output-warning-color, var(--verso-warning-indicator-color, #e7a71d));
401}
402
403.tippy-box[data-theme~='warning'] .hl.lean:not(.mixed) .hover-info.messages:not(:has(> code.error)):not(:has(> code.information)) > code.warning {
404  background: none;
405  border: none;
406}
407
408.warning .verso-message, .warning .verso-message .token, .warning .verso-message label {
409  color: var(--verso-message-warning-color, black);
410}
411
412.warning .verso-message .case-label:has(input[type="checkbox"])::before {
413  background-color: var(--verso-message-warning-color, black) !important;
414}
415
416
417.hl.lean .has-info.information {
418  --verso--region-indicator-color: var(--verso-info-indicator-color, #4777ff);
419  --verso--region-hover-color: var(--verso-code-info-hover-color, currentcolor);
420  --verso--region-hover-bg-color: var(--verso-code-info-hover-bg-color, #4777ff);
421  color: var(--verso-code-info-color, currentcolor);
422  background-color: var(--verso-code-info-bg-color, transparent);
423}
424
425
426.hl.lean .hover-info.messages > code.information {
427  background-color: var(--verso-tooltip-info-bg-color, #e5e5e5);
428  border-left: 0.2rem solid var(--verso-tooltip-info-border-color, #4777ff);
429}
430
431.tippy-box[data-theme~='info'] .hl.lean:not(.mixed) .hover-info.messages:not(:has(> code.error)):not(:has(> code.warning)) > code.information {
432  background: none;
433  border: none;
434}
435
436.information .verso-message, .information .verso-message .token, .information .verso-message label {
437  color: var(--verso-message-info-color, black);
438}
439
440.information .verso-message .case-label:has(input[type="checkbox"])::before {
441  background-color: var(--verso-message-info-color, black) !important;
442}
443
444.hl.lean div.docstring {
445  font-family: var(--verso-text-font-family, sans-serif);
446  white-space: normal;
447  max-width: calc(min(40rem, 90vw));
448  width: max-content;
449}
450
451.hl.lean div.docstring > :last-child {
452  margin-bottom: 0;
453}
454
455.hl.lean div.docstring > :first-child {
456  margin-top: 0;
457}
458
459.hl.lean .hover-info .sep {
460  display: block;
461  width: auto;
462  margin-left: 1rem;
463  margin-right: 1rem;
464  margin-top: 0.5rem;
465  margin-bottom: 0.5rem;
466  padding: 0;
467  height: 1px;
468  border-top: 1px solid var(--verso-tooltip-separator-color, #ccc);
469}
470
471.hl.lean code {
472  font-family: var(--verso-code-font-family);
473}
474
475.hl.lean .tactic-state {
476  display: none;
477  position: relative;
478  width: fit-content;
479  border: 1px solid var(--verso-tactic-state-border-color, #888888);
480  border-radius: 0.1rem;
481  padding: 0.5rem;
482  font-family: sans-serif;
483  color: var(--verso-tactic-state-color, black);
484  background-color: var(--verso-tactic-state-bg-color, white);
485}
486
487.hl.lean.popup .tactic-state {
488  position: static;
489  display: block;
490  width: auto;
491  border: none;
492  padding: 0.5rem;
493  font-family: sans-serif;
494  background-color: var(--verso-tactic-state-bg-color, white);
495}
496
497
498.hl.lean .tactic {
499  position: relative;
500  display: inline;
501  vertical-align: top;
502  /* Without these, mobile Safari will start making font sizes inconsistent when its text size adjustment feature is triggered.*/
503  -webkit-text-size-adjust: 100%;
504  text-size-adjust: 100%;
505}
506
507.hl.lean .tactic:has(> .tactic-toggle:checked) {
508  display: inline-grid;
509  grid-template-columns: 1fr;
510}
511
512.hl.lean .tactic-toggle:checked ~ .tactic-state {
513  display: inline-block;
514  vertical-align: top;
515  grid-row: 2;
516  justify-self: start;
517}
518
519.hl.lean .tactic > label {
520  position: relative;
521  grid-row: 1;
522  display: inline;
523}
524
525@media (hover: hover) {
526  /* Highlight a region on hover only when its own toggle is unchecked, and only the innermost
527     hovered region: `label:hover` bubbles to ancestor labels, so suppress the highlight on a region
528     whose label contains a more deeply nested hovered tactic label. The region's proof state is the
529     tooltip for everything else in its label, so the label keeps its highlight while any of that
530     content is hovered. */
531  .hl.lean .tactic:has(> .tactic-toggle:not(:checked)) > label:hover:not(:has(.tactic > label:hover)) {
532    background-color: var(--verso-code-hover-bg-color, #eeeeee);
533  }
534}
535
536.hl.lean .tactic-toggle {
537  position: absolute;
538  top: 0;
539  left: 0;
540  opacity: 0;
541  height: 0;
542  width: 0;
543  z-index: -10;
544}
545
546.hl.lean .tactic > label::after {
547  content: "";
548  border: 1px solid var(--verso-tactic-toggle-color, #bbbbbb);
549  /* These need to be em, not rem, to scale with the font */
550  border-radius: 1em;
551  height: 0.25em;
552  vertical-align: middle;
553  width: 0.6em;
554  margin-left: 0.1em;
555  margin-right: 0.1em;
556  display: inline-block;
557  transition: all 0.5s;
558}
559
560/*
561@media (hover: hover) {
562  .hl.lean .tactic > label:hover::after {
563    border: 1px solid #aaaaaa;
564    background-color: #aaaaaa;
565    transition: all 0.5s;
566  }
567}
568*/
569
570.hl.lean .tactic > label:has(+ .tactic-toggle:checked)::after {
571  border: 1px solid var(--verso-tactic-toggle-checked-color, #999999);
572  background-color: var(--verso-tactic-toggle-checked-color, #999999);
573  transition: all 0.5s;
574}
575
576.hl.lean .tactic-state .goal + .goal {
577  margin-top: 1.5em;
578}
579
580/*
581Some CSS frameworks customize details/summary in ways not compatible with Verso's output.
582*/
583
584.hl.lean details {
585  display: block !important;
586  margin: 0;
587}
588
589.hl.lean details summary {
590  display: list-item !important;
591  margin: 0;
592}
593
594.hl.lean details summary:focus {
595  outline: none;
596  outline-offset: none;
597  color: inherit;
598}
599
600.hl.lean ul > li {
601  margin-bottom: 0;
602}
603
604.hl.lean details summary::marker {
605  display: inline !important;
606}
607
608.hl.lean details > summary:first-of-type {
609  list-style-type: disclosure-closed;
610  list-style-position: inside;
611}
612
613.hl.lean details[open] > summary:first-of-type {
614  list-style-type: disclosure-open;
615}
616
617.hl.lean details summary::before, .hl.lean details summary::after {
618  content: "" !important;
619  background: none;
620  display: none;
621}
622
623.hl.lean .tactic-state summary {
624  /* These need to be em, not rem, to scale with the font */
625  margin-left: -0.5em;
626}
627
628.hl.lean .tactic-state details {
629  /* These need to be em, not rem, to scale with the font */
630  padding-left: 0.5em;
631}
632
633.hl.lean .case-label {
634  display: block;
635  position: relative;
636}
637
638.hl.lean .case-label input[type="checkbox"] {
639  position: absolute;
640  top: 0;
641  left: 0;
642  opacity: 0;
643  height: 0;
644  width: 0;
645  z-index: -10;
646}
647
648.hl.lean .case-label:has(input[type="checkbox"])::before {
649  display: inline-block;
650  background-color: currentcolor;
651  content: ' ';
652  transition: ease 0.2s;
653  margin-right: 0.7em;
654  clip-path: polygon(100% 0, 0 0, 50% 100%);
655  width: 0.6em;
656  height: 0.6em;
657  vertical-align: middle;
658}
659
660.hl.lean .case-label:has(input[type="checkbox"]:not(:checked))::before {
661  transform: rotate(-90deg);
662}
663
664.hl.lean .case-label:has(input[type="checkbox"]) {
665
666}
667
668.hl.lean .case-label:has(input[type="checkbox"]:checked) {
669
670}
671
672
673.hl.lean .labeled-case > :not(:first-child) {
674  max-height: 0px;
675  display: block;
676  overflow: hidden;
677  transition: max-height 0.1s ease-in;
678  /* These need to be em, not rem, to scale with the font */
679  margin-left: 0.5em;
680  margin-top: 0.1em;
681}
682
683.hl.lean .labeled-case:has(.case-label input[type="checkbox"]:checked) > :not(:first-child) {
684  max-height: 100%;
685}
686
687
688.hl.lean .goal-name::before {
689  font-style: normal;
690  content: "case ";
691}
692
693.hl.lean .goal-name {
694  font-style: italic;
695  font-family: var(--verso-code-font-family);
696  color: inherit;
697}
698
699.hl.lean .hypotheses {
700  display: table;
701}
702
703.hl.lean .hypothesis {
704  display: table-row;
705}
706
707.hl.lean .hypothesis > * {
708  display: table-cell;
709}
710
711
712.hl.lean .hypotheses .colon {
713  text-align: center;
714  /* This needs to be em, not rem, to scale with the font */
715  min-width: 1em;
716}
717
718.hl.lean .hypotheses .name {
719  text-align: right;
720}
721
722.hl.lean .hypotheses .name,
723.hl.lean .hypotheses .type,
724.hl.lean .conclusion .type {
725  font-family: var(--verso-code-font-family);
726}
727
728.tippy-box {
729  /* Without these, mobile Safari will start making font sizes inconsistent when its text size adjustment feature is triggered.*/
730  -webkit-text-size-adjust: 100%;
731  text-size-adjust: 100%;
732}
733
734/*
735Tippy's stylesheet paints each arrow's fill triangle with the arrow element's `color` (its
736placement-specific `::before` rules use `border-color: initial`, which is `currentcolor`),
737and its border extension paints the outline triangle with the box's border color. Setting
738`color` on the arrow therefore matches it to the tooltip background for every placement.
739*/
740.tippy-box[data-theme~='lean'] {
741  background-color: var(--verso-tooltip-bg-color, #e5e5e5);
742  color: var(--verso-tooltip-color, black);
743  border: 1px solid var(--verso-tooltip-border-color, black);
744}
745.tippy-box[data-theme~='lean'] > .tippy-arrow {
746  color: var(--verso-tooltip-bg-color, #e5e5e5);
747}
748
749.tippy-box[data-theme~='message'][data-placement^='top'] > .tippy-arrow::before {
750  border-width: 11px 11px 0;
751}
752.tippy-box[data-theme~='message'][data-placement^='top'] > .tippy-arrow::after {
753  bottom: -11px;
754  border-width: 11px 11px 0;
755}
756.tippy-box[data-theme~='message'][data-placement^='bottom'] > .tippy-arrow::before {
757  border-width: 0 11px 11px;
758}
759.tippy-box[data-theme~='message'][data-placement^='bottom'] > .tippy-arrow::after {
760  top: -11px;
761  border-width: 0 11px 11px;
762}
763.tippy-box[data-theme~='message'][data-placement^='left'] > .tippy-arrow::before {
764  border-width: 11px 0 11px 11px;
765}
766.tippy-box[data-theme~='message'][data-placement^='left'] > .tippy-arrow::after {
767  right: -11px;
768  border-width: 11px 0 11px 11px;
769}
770
771.tippy-box[data-theme~='message'][data-placement^='right'] > .tippy-arrow::before {
772  border-width: 11px 11px 11px 0;
773}
774.tippy-box[data-theme~='message'][data-placement^='right'] > .tippy-arrow::after {
775  left: -11px;
776  border-width: 11px 11px 11px 0;
777}
778
779
780
781.tippy-box[data-theme~='warning'] {
782  background-color: var(--verso-tooltip-warning-bg-color, #e5e5e5);
783  color: var(--verso-tooltip-warning-color, black);
784  border: 3px solid var(--verso-tooltip-warning-border-color, #ffd580);
785}
786.tippy-box[data-theme~='warning'] > .tippy-arrow {
787  color: var(--verso-tooltip-warning-bg-color, #e5e5e5);
788}
789
790.tippy-box[data-theme~='error'] {
791  background-color: var(--verso-tooltip-error-bg-color, #e5e5e5);
792  color: var(--verso-tooltip-error-color, black);
793  border: 3px solid var(--verso-tooltip-error-border-color, #ffb3b3);
794}
795.tippy-box[data-theme~='error'] > .tippy-arrow {
796  color: var(--verso-tooltip-error-bg-color, #e5e5e5);
797}
798
799.tippy-box[data-theme~='info'] {
800  background-color: var(--verso-tooltip-info-bg-color, #e5e5e5);
801  color: var(--verso-tooltip-info-color, black);
802  border: 3px solid var(--verso-tooltip-info-border-color, #4777ff);
803}
804.tippy-box[data-theme~='info'] > .tippy-arrow {
805  color: var(--verso-tooltip-info-bg-color, #e5e5e5);
806}
807
808.tippy-box[data-theme~='tactic'] {
809  background-color: var(--verso-tactic-state-bg-color, white);
810  color: var(--verso-tactic-state-color, black);
811  border: 1px solid var(--verso-tactic-state-border-color, #888888);
812}
813.tippy-box[data-theme~='tactic'] > .tippy-arrow {
814  color: var(--verso-tactic-state-bg-color, white);
815}
816
817.extra-doc-links {
818  list-style-type: none;
819  margin-left: 0;
820  padding: 0;
821}
822
823.extra-doc-links > li {
824  display: inline-block;
825}
826
827.extra-doc-links > li:not(:last-child)::after {
828  content: '|';
829  display: inline-block;
830  margin: 0 0.25em;
831}
832
833.verso-message .trace {
834  display: block;
835}
836
837.verso-message .trace > summary::marker {
838  color: var(--verso-text-color, black);
839}
840
841.verso-message .trace-children {
842  margin: 0;
843  padding: 0;
844}
845
846.verso-message .trace-children > li {
847  list-style-type: none;
848  margin-left: 1.5em;
849}
850
851.verso-message .trace-children > li:not(:has(.trace)) {
852  margin-left: 0;
853}
854
855.verso-message .trace-class {
856  color: color-mix(in srgb, currentColor 70%, transparent);
857  font-weight: bold;
858  margin: 0;
859  padding: 0;
860}
861
862.verso-message .text {
863  white-space: pre-wrap;
864}
865
866
867</style>
868<script>
869      
870
871window.onload = async () => {
872
873    // Don't show hovers inside of closed tactic states
874    function blockedByTactic(elem) {
875      let parent = elem.parentNode;
876      while (parent && "classList" in parent) {
877        if (parent.classList.contains("tactic")) {
878          const toggle = parent.querySelector(":scope > input.tactic-toggle");
879          if (toggle) {
880            return !toggle.checked;
881          }
882        }
883        parent = parent.parentNode;
884      }
885      return false;
886    }
887
888    // The innermost element under the pointer, used to show only the most specific hover
889    let hoverTarget = null;
890    document.addEventListener('mouseover', (e) => { hoverTarget = e.target; }, true);
891
892    // Visible tippy references; a tooltip is blocked while an unrelated one is visible
893    const visibleTippies = new Set();
894    function blockedByTippy(elem) {
895      for (const ref of visibleTippies) {
896        if (!ref.contains(elem) && !elem.contains(ref)) return true;
897      }
898      return false;
899    }
900
901    // Whether the element's tooltip would have content to show. Content nested in a
902    // collapsed tactic region is covered by the region's proof-state tooltip, whether or
903    // not a tippy instance is currently attached to it.
904    function showsContent(el) {
905      if (!el._tippy) return false;
906      if (el.classList.contains('tactic')) {
907        const toggle = el.querySelector(':scope > input.tactic-toggle');
908        return !!toggle && !toggle.checked;
909      }
910      return (!!el.querySelector('.hover-info') || 'versoHover' in el.dataset) &&
911        !blockedByTactic(el);
912    }
913
914    // The nearest enclosing element whose tooltip has content
915    function innermostShowable(el) {
916      while (el && el.nodeType === Node.ELEMENT_NODE) {
917        if (showsContent(el)) return el;
918        el = el.parentElement;
919      }
920      return null;
921    }
922
923    // Binding highlights via event delegation with cached lookups
924    const bindingCache = new Map(); // context+binding -> [token elements]
925    let highlightedTokens = [];
926    function getBindingTokens(context, binding) {
927      const key = context + "\0" + binding;
928      let tokens = bindingCache.get(key);
929      if (!tokens) {
930        tokens = [];
931        for (const example of document.querySelectorAll(".hl.lean")) {
932          if (example.dataset.leanContext == context) {
933            for (const tok of example.querySelectorAll(".token[data-binding=\"" + CSS.escape(binding) + "\"]")) {
934              tokens.push(tok);
935            }
936          }
937        }
938        bindingCache.set(key, tokens);
939      }
940      return tokens;
941    }
942    for (const container of document.querySelectorAll(".hl.lean")) {
943      container.addEventListener("mouseover", (event) => {
944        const c = event.target.closest(".token");
945        if (!c || !c.dataset.binding || c.dataset.binding === "" || !container.contains(c)) return;
946        if (blockedByTactic(c)) return;
947        const tokens = getBindingTokens(container.dataset.leanContext, c.dataset.binding);
948        for (const tok of tokens) {
949          tok.classList.add("binding-hl");
950        }
951        highlightedTokens = tokens;
952      });
953      container.addEventListener("mouseout", (event) => {
954        const c = event.target.closest(".token");
955        if (!c || !container.contains(c)) return;
956        for (const tok of highlightedTokens) {
957          tok.classList.remove("binding-hl");
958        }
959        highlightedTokens = [];
960      });
961    }
962    /* Render docstrings */
963    if ('undefined' !== typeof marked) {
964        for (const d of document.querySelectorAll("code.docstring, pre.docstring")) {
965            const str = d.innerText;
966            const html = marked.parse(str);
967            const rendered = document.createElement("div");
968            rendered.classList.add("docstring");
969            rendered.innerHTML = html;
970            d.parentNode.replaceChild(rendered, d);
971        }
972    }
973    // Add hovers
974    const versoDocData = await (fetch("-verso-docs.json").then((resp) => resp.json()));
975
976    function hideParentTooltips(element) {
977      let parent = element.parentElement;
978      while (parent) {
979        const tippyInstance = parent._tippy;
980        if (tippyInstance) {
981          tippyInstance.hide();
982        }
983        parent = parent.parentElement;
984      }
985    }
986
987    function hideDescendantTooltips(element) {
988      for (const ref of visibleTippies) {
989        if (ref !== element && element.contains(ref)) {
990          ref._tippy.hide();
991        }
992      }
993    }
994
995    // Renders the documentation for a hover ID from the doc table
996    function docHoverContent(hoverId) {
997      const info = document.createElement('span');
998      info.className = 'hover-info';
999      info.style.display = 'block';
1000      const data = versoDocData[hoverId];
1001      if (data) {
1002        info.innerHTML = data;
1003        /* Render docstrings - TODO server-side */
1004        if ('undefined' !== typeof marked) {
1005          for (const d of info.querySelectorAll('code.docstring, pre.docstring')) {
1006            const str = d.innerText;
1007            const html = marked.parse(str);
1008            const rendered = document.createElement('div');
1009            rendered.classList.add('docstring');
1010            rendered.innerHTML = html;
1011            d.parentNode.replaceChild(rendered, d);
1012          }
1013        }
1014      } else {
1015        info.innerHTML = 'Failed to load doc ID: ' + hoverId;
1016      }
1017      return info;
1018    }
1019
1020
1021
1022
1023    const defaultTippyProps = {
1024      /* DEBUG -- remove the space: * /
1025      onHide(any) { return false; },
1026      trigger: "click",
1027      // */
1028      /* theme: "lean", */
1029      maxWidth: "none",
1030      appendTo: () => document.body,
1031      interactive: true,
1032      delay: [100, null],
1033      /* ignoreAttributes: true, */
1034      followCursor: 'initial',
1035      onShow(inst) {
1036        const ref = inst.reference;
1037        if (ref.className == 'tactic') {
1038          const toggle = ref.querySelector(":scope > input.tactic-toggle");
1039          if (toggle && toggle.checked) {
1040            return false;
1041          }
1042        } else if (ref.querySelector(".hover-info") || "versoHover" in ref.dataset) {
1043          if (blockedByTactic(ref)) { return false };
1044        } else { // Nothing to show here!
1045          return false;
1046        }
1047        // Show only the most specific hover under the pointer
1048        if (hoverTarget && ref.contains(hoverTarget) && innermostShowable(hoverTarget) !== ref) {
1049          return false;
1050        }
1051        hideParentTooltips(ref);
1052        hideDescendantTooltips(ref);
1053        if (blockedByTippy(ref)) { return false; }
1054      },
1055      onShown(inst) { visibleTippies.add(inst.reference); },
1056      onHidden(inst) { visibleTippies.delete(inst.reference); },
1057      content (tgt) {
1058        const content = document.createElement("span");
1059        if (tgt.className == 'tactic') {
1060          const state = tgt.querySelector(":scope > .tactic-state").cloneNode(true);
1061          state.style.display = "block";
1062          content.appendChild(state);
1063          content.style.display = "block";
1064          content.className = "hl lean popup";
1065        } else {
1066          content.className = "hl lean";
1067          content.style.display = "block";
1068          content.style.maxHeight = "300px";
1069          content.style.overflowY = "auto";
1070          content.style.overflowX = "hidden";
1071          // Messages come from the inline hover-info; documentation comes from the doc
1072          // table. An element with both (a message span sharing a documented token's
1073          // extent) shows both in one tooltip.
1074          const hoverId = tgt.dataset.versoHover;
1075          const hoverInfo = tgt.querySelector(".hover-info");
1076          if (hoverInfo) {
1077            content.appendChild(hoverInfo.cloneNode(true));
1078          }
1079          if (hoverId) {
1080            // TODO stop doing an implicit conversion from string to number here
1081            content.appendChild(docHoverContent(hoverId));
1082          }
1083          if (hoverInfo && hoverId) {
1084            content.classList.add('mixed');
1085          }
1086          const extraLinks = tgt.dataset['versoLinks'] || tgt.parentElement.dataset['versoLinks'];
1087          if (extraLinks) {
1088            try {
1089              const extras = JSON.parse(extraLinks);
1090              const links = document.createElement('ul');
1091              links.className = 'extra-doc-links';
1092              extras.forEach((l) => {
1093                const li = document.createElement('li');
1094                li.innerHTML = "<a href=\"" + l['href'] + "\" title=\"" + l.long + "\">" + l.short + "</a>";
1095                links.appendChild(li);
1096              });
1097              content.appendChild(links);
1098            } catch (error) {
1099              console.error(error);
1100            }
1101          }
1102        }
1103        return content;
1104      }
1105    };
1106
1107
1108    document.querySelectorAll('.hl.lean .const.token, .hl.lean .keyword.token, .hl.lean .literal.token, .hl.lean .option.token, .hl.lean .var.token, .hl.lean .typed.token, .hl.lean .level-var, .hl.lean .level-const, .hl.lean .level-op, .hl.lean .sort').forEach(element => {
1109      element.setAttribute('data-tippy-theme', 'lean');
1110    });
1111    document.querySelectorAll('.hl.lean .has-info.warning').forEach(element => {
1112      element.setAttribute('data-tippy-theme', 'warning message');
1113    });
1114    document.querySelectorAll('.hl.lean .has-info.information').forEach(element => {
1115      element.setAttribute('data-tippy-theme', 'info message');
1116    });
1117    document.querySelectorAll('.hl.lean .has-info.error').forEach(element => {
1118      element.setAttribute('data-tippy-theme', 'error message');
1119    });
1120    document.querySelectorAll('.hl.lean .tactic').forEach(element => {
1121      element.setAttribute('data-tippy-theme', 'tactic');
1122    });
1123    // Skip tokens inside closed tactics — they interfere with tactic tippys
1124    const closedTactics = new Set();
1125    document.querySelectorAll('.hl.lean .tactic').forEach(tactic => {
1126      const toggle = tactic.querySelector(':scope > input.tactic-toggle');
1127      if (toggle && !toggle.checked) closedTactics.add(tactic);
1128    });
1129    function isInsideClosedTactic(el) {
1130      const tactic = el.closest('.tactic');
1131      return tactic && tactic !== el && closedTactics.has(tactic);
1132    }
1133
1134    const tokenSelector = '.hl.lean .const.token, .hl.lean .keyword.token, .hl.lean .literal.token, .hl.lean .option.token, .hl.lean .var.token, .hl.lean .typed.token, .hl.lean .has-info, .hl.lean .tactic, .hl.lean .level-var, .hl.lean .level-const, .hl.lean .level-op, .hl.lean .sort';
1135    tippy(Array.from(document.querySelectorAll(tokenSelector)).filter(el => !isInsideClosedTactic(el)), defaultTippyProps);
1136
1137    // Create/destroy token tippys when tactic checkbox toggles
1138    const tacticTippySelector = '.const.token, .keyword.token, .literal.token, .option.token, .var.token, .typed.token, .has-info, .level-var, .level-const, .level-op, .sort';
1139    document.querySelectorAll('.hl.lean .tactic').forEach(tactic => {
1140      const toggle = tactic.querySelector(':scope > input.tactic-toggle');
1141      if (toggle) toggle.addEventListener('change', () => {
1142        if (toggle.checked) {
1143          closedTactics.delete(tactic);
1144          tactic.querySelectorAll(tacticTippySelector).forEach(el => {
1145            if (!el._tippy) {
1146              tippy(el, defaultTippyProps);
1147            }
1148          });
1149        } else {
1150          closedTactics.add(tactic);
1151          tactic.querySelectorAll(tacticTippySelector).forEach(el => {
1152            if (el._tippy) el._tippy.destroy();
1153          });
1154        }
1155        // The toggle changes which element's tooltip belongs to the pointer's position,
1156        // but the pointer stays put, so no hover event announces the change. Show the
1157        // right tooltip once the click that flipped the toggle has hidden the old one.
1158        setTimeout(() => {
1159          if (hoverTarget && hoverTarget.isConnected) {
1160            const showable = innermostShowable(hoverTarget);
1161            if (showable && showable._tippy) showable._tippy.show();
1162          }
1163        }, 0);
1164      });
1165  });
1166}
1167
1168</script>
1168
1169    
1170<script>
1171      
1172document.addEventListener("DOMContentLoaded", () => {
1173    for (const m of document.querySelectorAll(".math.inline")) {
1174        katex.render(m.textContent, m, {throwOnError: false, displayMode: false});
1175    }
1176    for (const m of document.querySelectorAll(".math.display")) {
1177        katex.render(m.textContent, m, {throwOnError: false, displayMode: true});
1178    }
1179});
1180</script>
1180
1181    
1182<script src="-verso-data/dark.js"></script>
1182
1183    
1183<script src="-verso-data/theme.js"></script>
1183
1184    
1184<script src="-verso-data/copy.js"></script>
1184
1185    
1185<script src="-verso-data/motion.js"></script>
1185
1186    
1186<script src="-verso-data/navbar.js"></script>
1186
1187    
1187<script src="-verso-data/popper.js"></script>
1187
1188    
1188<script src="-verso-data/tippy.js"></script>
1188
1189    
1189<script src="-verso-data/testimonials.js"></script>
1189
1190    
1190<script src="-verso-data/glightbox.min.js"></script>
1190
1191    
1191<script src="-verso-data/gallery.js"></script>
1191
1192    
1192<script src="-verso-data/fro.js"></script>
1192
1193    <link rel="stylesheet" href="-verso-data/reset.css">
1194    <link rel="stylesheet" href="-verso-data/layout.css">
1195    <link rel="stylesheet" href="-verso-data/navbar.css">
1196    <link rel="stylesheet" href="-verso-data/footer.css">
1197    <link rel="stylesheet" href="-verso-data/theme.css">
1198    <link rel="stylesheet" href="-verso-data/article.css">
1199    <link rel="stylesheet" href="-verso-data/card.css">
1200    <link rel="stylesheet" href="-verso-data/copy-button.css">
1201    <link rel="stylesheet" href="-verso-data/tippy-border.css">
1202    <link rel="stylesheet" href="-verso-data/action.css">
1203    <link rel="stylesheet" href="-verso-data/timeline.css">
1204    <link rel="stylesheet" href="-verso-data/testimonials.css">
1205    <link rel="stylesheet" href="-verso-data/steps.css">
1206    <link rel="stylesheet" href="-verso-data/glightbox.css">
1207    <link rel="stylesheet" href="-verso-data/gallery.css">
1208    <link rel="stylesheet" href="-verso-data/zulipInfo.css">
1209    <link rel="stylesheet" href="-verso-data/org-hero.css">
1210    <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.css" integrity="sha384-n8MVd4RsNIU0tAv4ct0nTaAbDJwPJzDEaqSD1odI+WdtXRGWt2kTvGFasHpSy3SV" crossorigin="anonymous">
1211    
1211<script defer="defer" src="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.js" integrity="sha384-XjKyOOlGwcjNTAIQHIpgOno0Hl1YQqzUOEleOLALmuqehneUG+vnGctmUb0ZY0l8" crossorigin="anonymous"></script>
1211
1212    
1212<script src="https://cdn.jsdelivr.net/npm/[email protected]/marked.min.js" integrity="sha384-zbcZAIxlvJtNE3Dp5nxLXdXtXyxwOdnILY1TDPVmKFhl4r4nSUG1r8bcFXGVa4Te" crossorigin="anonymous"></script>
1212
1213    <style>
1214
1215    @media (scripting: none) {
1216      #selector-input---verso-component-5-2:checked ~ .selector-list .selector-button[for="selector-input---verso-component-5-2"] {
1217        background-color: var(--color-primary);
1218        color: white;
1219      }
1220
1221      #--verso-component-5-panel-2 {
1222        display: none;
1223      }
1224
1225      #selector-input---verso-component-5-2:checked ~ .selector-panels > #--verso-component-5-panel-2 {
1226        display: block;
1227      }
1228    }
1229  
1230</style>
1231<style>
1232.sponsors-section {
1233    background: var(--color-white);
1234    padding: var(--space-16) 0;
1235}
1236
1237.dark-theme .sponsors-section {
1238    background: #111;
1239}
1240
1241.sponsors {
1242    display: flex;
1243    flex-direction: column;
1244    align-content: center;
1245    align-items: center;
1246}
1247
1248.sponsors-content {
1249    display: grid;
1250    grid-template-columns: repeat(3, 1fr);
1251    max-width: 900px;
1252    width: 100%;
1253}
1254
1255.sponsor {
1256    min-height: 95px;
1257    display: flex;
1258    align-items: center;
1259    justify-content: center;
1260    padding: var(--space-8) var(--space-6);
1261}
1262
1263/* centre a sponsor that ends up alone on the last row */
1264.sponsor:last-child:nth-child(3n+1):not(:first-child) {
1265    grid-column: 2;
1266}
1267
1268img.sponsor-logo {
1269    width: 100%;
1270    max-width: 250px;
1271    max-height: 90px;
1272    object-fit: contain;
1273    opacity: 0.8;
1274    transition: opacity var(--transition-base);
1275}
1276
1277.sponsor:hover img.sponsor-logo {
1278    opacity: 1;
1279}
1280
1281@media (max-width: 768px) {
1282    .sponsors {
1283        width: calc(100% - var(--space-8)*2);
1284    }
1285
1286    .sponsors-content {
1287        grid-template-columns: repeat(2, 1fr);
1288        width: 100%;
1289    }
1290
1291    /* two columns leave no middle to centre in, so a lone sponsor spans the row */
1292    .sponsor:last-child:nth-child(odd):not(:first-child) {
1293        grid-column: 1 / -1;
1294    }
1295}
1296
1297.dark-theme .sponsor-logo {
1298    filter: invert(1) brightness(10);
1299}
1300
1301/* Sponsors that ship a dedicated dark logo swap the image instead of inverting it. */
1302.sponsor-logo-dark {
1303    display: none;
1304}
1305
1306.dark-theme .sponsor-logo-light {
1307    display: none;
1308}
1309
1310.dark-theme .sponsor-logo-dark {
1311    display: block;
1312}
1313
1314.dark-theme .sponsor-logo-light,
1315.dark-theme .sponsor-logo-dark {
1316    filter: none;
1317}
1318
1319</style>
1320<style>
1321.button {
1322    border-radius: var(--radius-md);
1323    padding: var(--space-4) var(--space-12);
1324    display: flex;
1325    align-items: center;
1326    gap: var(--space-3);
1327    justify-content: center;
1328    font-size: var(--fs-md);
1329    font-weight: 500;
1330    cursor: pointer;
1331    transition: all var(--transition-base);
1332}
1333
1334a.primary {
1335    background: var(--color-primary);
1336    color: var(--color-text-contrast);
1337    fill: var(--color-text-contrast);
1338}
1339
1340a.primary svg {
1341    fill: var(--color-text-contrast);
1342}
1343
1344a.primary:hover {
1345    background: var(--color-primary-light) !important;
1346    color: var(--color-text-contrast) !important;
1347    border: 0px !important;
1348}
1349
1350a.primary:focus {
1351    background: var(--color-primary-focus);
1352    color: var(--color-text-contrast);
1353}
1354
1355.secondary {
1356    border: 2px solid var(--color-primary);
1357    background: var(--color-white);
1358    color: var(--color-primary);
1359}
1360
1361.secondary:hover {
1362    background: var(--color-primary);
1363    fill: var(--color-text-contrast);
1364    color: var(--color-text-contrast);
1365}
1366
1367.secondary:hover svg {
1368    fill: var(--color-text-contrast);
1369}
1370
1371.primary.inverted {
1372    background: var(--color-text-contrast);
1373    color: var(--color-primary);
1374    fill: var(--color-primary);
1375}
1376
1377.primary.inverted svg {
1378    fill: var(--color-text-contrast);
1379}
1380
1381.primary.inverted:hover {
1382    background: #e9e9e9;
1383}
1384
1385.primary.inverted:focus {
1386    background: var(--color-primary-focus);
1387    color: var(--color-text-contrast);
1388}
1389
1390.secondary.inverted {
1391    border: 2px solid var(--color-text-contrast);
1392    background: transparent;
1393    color: var(--color-text-contrast);
1394}
1395
1396.secondary.inverted:hover {
1397    background: var(--color-text-contrast);
1398    fill: var(--color-primary);
1399    color: var(--color-primary);
1400}
1401
1402.secondary.inverted:hover svg {
1403    fill: var(--color-white);
1404}
1405</style>
1406<style>
1407
1408    @media (scripting: none) {
1409      #selector-input---verso-component-5-0:checked ~ .selector-list .selector-button[for="selector-input---verso-component-5-0"] {
1410        background-color: var(--color-primary);
1411        color: white;
1412      }
1413
1414      #--verso-component-5-panel-0 {
1415        display: none;
1416      }
1417
1418      #selector-input---verso-component-5-0:checked ~ .selector-panels > #--verso-component-5-panel-0 {
1419        display: block;
1420      }
1421    }
1422  
1423</style>
1424<style>
1425.card-grid {
1426    display: grid;
1427    grid-template-columns: repeat(2, 1fr);
1428    gap: 16px;
1429}
1430
1431.card-grid > :last-child:nth-child(odd) {
1432    grid-column: span 2;
1433}
1434
1435.main-learn-card {
1436    display: flex;
1437    flex-direction: column;
1438    transition: background-color var(--transition-base), border-color var(--transition-base);
1439    justify-content: space-between;
1440    padding: 40px;
1441    align-content: center;
1442    gap: 20px;
1443}
1444
1445a.card-href.card.main-learn-card {
1446    position: relative;
1447    background: var(--card-bg);
1448    border: 1px solid var(--color-border) !important;
1449    border-radius: var(--radius-md);
1450    transition: background-color var(--transition-base), border-color var(--transition-base);
1451    height: 100%;
1452    box-sizing: border-box;
1453}
1454
1455.card-title {
1456    margin: 0px !important;
1457    font-size: 1.15rem !important;
1458    line-height: 1.4 !important;
1459    display: flex;
1460    align-items: center;
1461    font-weight: 600 !important;
1462    color: var(--color-text) !important;
1463    transition: color var(--transition-base);
1464    padding: 0px !important;
1465    border-bottom: none !important;
1466}
1467
1468.main-learn-card header {
1469    display: flex;
1470    flex-direction: column;
1471    gap: var(--gap-lg);
1472    text-align: center;
1473    align-items: center;
1474    background: var(--color-primary);
1475    border-radius: 7px;
1476    height: 220px;
1477    color: white;
1478    justify-content: center;
1479    margin-bottom: 20px;
1480    display: none;
1481}
1482
1483.card-description {
1484    margin: 0px 0px !important;
1485    color: var(--color-text) !important;
1486    transition: color var(--transition-base);
1487}
1488
1489a.card-button {
1490    color: var(--color-text-contrast);
1491    display: block;
1492    text-decoration: none;
1493    transition: background-color var(--transition-base), color var(--transition-base);
1494    cursor: pointer;
1495    margin: 10px;
1496}
1497
1498a.card-button:hover {
1499    background-color: var(--color-primary-light);
1500}
1501
1502.main-learn-card footer {
1503    width: fit-content;
1504    color: black;
1505}
1506
1507.card-body {
1508    padding: 30px 60px;
1509}
1510
1511@media (max-width: 768px) {
1512    .wrap {
1513        padding-top: 20px;
1514    }
1515
1516    .main-learn-card {
1517        flex-direction: column;
1518    }
1519
1520    .card-body {
1521        padding: 10px;
1522    }
1523}
1524
1525.main-learn-card .read-more {
1526    border: none;
1527    background: none !important;
1528    color: var(--color-primary);
1529}
1530
1531.main-learn-card .read-more:hover {
1532    border-bottom: 0px;
1533    background-color: var(--color-primary-light) !important;
1534}
1535
1536.main-learn-card .read-more svg {
1537    fill: var(--color-primary) !important;
1538}
1539
1540.main-learn-card:hover .read-more svg {
1541    transform: translateX(4px);
1542    opacity: 1;
1543}
1544
1545.main-learn-card .read-more:hover {
1546    background: none !important;
1547}
1548
1549.item-tag {
1550    background: #f1f5f9;
1551    color: #64748b;
1552    padding: 4px 12px;
1553    border-radius: 16px;
1554    font-size: 0.8rem;
1555    font-weight: 500;
1556}
1557
1558.tags {
1559    display: flex;
1560    gap: 15px;
1561    padding-top: 10px;
1562    margin-top: auto;
1563    flex-wrap: wrap;
1564}
1565
1566.dark-theme .item-tag {
1567    color: var(--color-text);
1568    background: var(
1569    --color-bg);
1570}
1571
1572@media (max-width: 768px) {
1573    .wrap {
1574        padding-top: 20px;
1575    }
1576
1577    .card-body {
1578        padding: 10px;
1579    }
1580}
1581
1582@media (max-width: 1024px) {
1583    .card-grid {
1584        display: flex;
1585        flex-direction: column;
1586        gap: 20px;
1587    }
1588
1589    .main-learn-card {
1590        display: flex;
1591        flex-direction: column;
1592    }
1593}
1594</style>
1595<style>
1596.read-more {
1597    font-weight: bold;
1598    text-transform: uppercase;
1599    font-size: var(--fs-sm);
1600    display: flex;
1601    align-items: center;
1602    gap: 5px;
1603    color: var(--color-text);
1604    margin-top: auto;
1605}
1606
1607.read-more svg {
1608    fill: var(--color-text) !important;
1609    transition: transform 0.2s, opacity 0.2s;
1610    opacity: 1;
1611}
1612
1613.read-more:hover svg {
1614    transform: translateX(4px);
1615    opacity: 1;
1616}
1617</style>
1618<style>
1619.code-gallery-tip {
1620    display: none;
1621    align-items: center;
1622    gap: 20px;
1623    color: var(--color-text-light);
1624    justify-content: space-between;
1625    width: 100%;
1626}
1627
1628.code-gallery-tip.active {
1629    display: flex;
1630}
1631
1632.code-gallery-box {
1633    background-color: var(--color-white);
1634    border: 2px solid var(--color-primary);
1635    border-radius: var(--radius-lg);
1636    display: flex;
1637    flex-direction: column;
1638    position: relative;
1639    overflow: hidden;
1640    box-shadow:
1641        0px 124px 74px rgba(35, 55, 139, 0.01),
1642        0px 55px 55px rgba(35, 55, 139, 0.04),
1643        0px 0px 4px rgba(208, 241, 255, 0.25);
1644    width: 100%;
1645    box-sizing: border-box;
1646    height: 515px;
1647}
1648
1649.code-gallery-tabs {
1650    display: flex;
1651    position: relative;
1652    overflow-x: auto;
1653}
1654
1655.code-gallery-tab {
1656    padding: var(--space-3) var(--space-8);
1657    background-color: var(--color-white);
1658    border-bottom: 2px solid var(--color-border);
1659    cursor: pointer;
1660    white-space: nowrap;
1661}
1662
1663.code-gallery-tab.active {
1664    color: var(--color-primary);
1665}
1666
1667.code-gallery-tab.filler {
1668    flex: 1;
1669}
1670
1671.code-gallery-tab-border {
1672    position: absolute;
1673    bottom: 0;
1674    height: 2px;
1675    background: var(--color-primary);
1676    transition: left 0.3s ease, width 0.3s ease;
1677    z-index: 0;
1678}
1679
1680.code-gallery-content {
1681    font-family: monospace;
1682    font-size: 0.9rem;
1683    flex: 1;
1684    line-height: 1.7;
1685    min-height: 300px;
1686    position: relative;
1687    overflow: auto;
1688}
1689
1690.code-gallery-snippet.visible-code {
1691    padding: var(--space-4);
1692    display: block;
1693}
1694
1695.code-gallery-snippet {
1696    display: none;
1697}
1698
1699.code-gallery-footer {
1700    min-height: 70px;
1701    border-top: 1px solid var(--color-border);
1702    display: flex;
1703    padding: 10px 30px;
1704    align-items: center;
1705    gap: 10px;
1706    justify-content: space-between;
1707}
1708
1709.hero-footer-left {
1710    display: flex;
1711    gap: var(--gap-md);
1712    line-height: 1.4;
1713    width: 100%;
1714}
1715
1716.code-gallery-next {
1717    position: absolute;
1718    bottom: -2rem;
1719    right: var(--space-4);
1720    padding: 0.3rem 0.8rem;
1721    border: 1px solid var(--color-primary);
1722    border-radius: var(--radius-sm);
1723    background: var(--color-white);
1724    color: var(--color-primary);
1725    font-weight: bold;
1726    display: flex;
1727    align-items: center;
1728    justify-content: center;
1729    cursor: pointer;
1730}
1731
1732.code-block-wrapper {
1733    position: relative;
1734}
1735
1736.hl.lean span {
1737    color: var(--color-text) !important;
1738}
1739
1740</style>
1741<style>
1742.archive-content {
1743    display: flex;
1744    flex-direction: column;
1745    gap: 15px;
1746    transition: background-color var(--transition-base), border-color var(--transition-base);
1747    padding: var(--space-12);
1748}
1749
1750.archive-content .metadata {
1751    display: flex;
1752    gap: 0px;
1753    font-size: var(--fs-sm);
1754    color: var(--color-text-light);
1755}
1756
1757.archive-content .metadata :not(:last-child)::after {
1758    content: "·";
1759    margin-left: 0.5rem;
1760}
1761
1762.use-cases-grid ul.post-list {
1763    display: grid;
1764    grid-template-columns: calc(50% - 25px) calc(50% - 25px);
1765}
1766
1767@media (max-width: 1024px) {
1768    .use-cases-grid ul.post-list {
1769        display: flex;
1770    }
1771}
1772
1773/* Fix */
1774
1775.features-heading {
1776    gap: 70px;
1777    display: flex;
1778    flex-direction: column;
1779}
1780
1781
1782ul.post-list {
1783    padding-bottom: 100px;
1784    display: flex;
1785    flex-direction: column;
1786    gap: 20px;
1787    padding: 0px !important;
1788    margin: 0px !important;
1789    margin-top: 3.5rem !important;
1790}
1791
1792.post-list li {
1793    background-color: var(--card-bg);
1794    border: 1px solid var(--color-border-light);
1795    border-radius: var(--radius-md);
1796    overflow: hidden;
1797    font-size: var(--fs-md);
1798    transition: background-color var(--transition-base), border-color var(--transition-base);
1799}
1800
1801.title span.name {
1802    line-height: 1.2;
1803    font-size: 1.3rem;
1804    font-weight: bold;
1805    color: var(--color-text);
1806    transition: color var(--transition-base);
1807}
1808
1809.post-list li a {
1810    color: var(--color-text) !important;
1811    transition: color var(--transition-base);
1812    border: none !important;
1813    background: none !important;
1814}
1815
1816.page-content {
1817    padding-bottom: 0;
1818}
1819
1820a.read-more {
1821    font-weight: bold;
1822    text-transform: uppercase;
1823    font-size: var(--fs-sm);
1824    display: flex;
1825    align-items: center;
1826    gap: 5px;
1827}
1828
1829.post-list li, .post-list p {
1830    color: var(--color-text-light) !important;
1831    line-height: 1.6 !important;
1832    margin: 0px !important;
1833}
1834
1835.metadata {
1836    display: flex;
1837    gap: 0px;
1838    font-size: var(--fs-sm);
1839    color: var(--color-text-light);
1840}
1841
1842.metadata :not(:last-child)::after {
1843    content: "·";
1844    margin-left: 0.5rem;
1845}
1846
1847.post-list li:hover .read-more svg {
1848    transform: translateX(4px);
1849    opacity: 1;
1850}
1851
1852.blog-page {
1853    padding-top: 0px !important
1854}
1855
1856@media (max-width: 768px) {
1857    .wrap {
1858        padding-top: var(--space-8);
1859    }
1860
1861    .title span.name {
1862        font-size: var(--fs-lg);
1863    }
1864
1865}
1866
1867.archive-content {
1868    display: flex;
1869    flex-direction: column;
1870    gap: 15px;
1871    transition: background-color var(--transition-base), border-color var(--transition-base);
1872    padding: var(--space-12);
1873}
1874
1875.post-list li img {
1876    height: 200px;
1877    object-fit: cover;
1878    width: 100%;
1879    margin: 0px;
1880    border-radius: 0px;
1881    box-shadow: none;
1882}
1883</style>
1884<style>
1885
1886    @media (scripting: none) {
1887      #selector-input---verso-component-5-1:checked ~ .selector-list .selector-button[for="selector-input---verso-component-5-1"] {
1888        background-color: var(--color-primary);
1889        color: white;
1890      }
1891
1892      #--verso-component-5-panel-1 {
1893        display: none;
1894      }
1895
1896      #selector-input---verso-component-5-1:checked ~ .selector-panels > #--verso-component-5-panel-1 {
1897        display: block;
1898      }
1899    }
1900  
1901</style>
1902<style>
1903.gallery-card-content,
1904.gallery-card-image {
1905    flex: 1;
1906}
1907
1908.gallery-card-content {
1909    padding: var(--space-12);
1910    display: flex;
1911    flex-direction: column;
1912    justify-content: start;
1913    gap: 20px;
1914}
1915
1916.gallery-tag {
1917    font-size: var(--fs-xs);
1918    font-weight: bold;
1919    color: var(--color-text-contrast);
1920    text-transform: uppercase;
1921    background: var(--color-primary);
1922    width: fit-content;
1923    padding: var(--space-1) var(--space-6);
1924    border-radius: var(--radius-pill);
1925}
1926
1927.gallery-title {
1928    font-size: var(--fs-xl);
1929    font-weight: 700;
1930    color: var(--color-text);
1931}
1932
1933.gallery-description {
1934    font-size: var(--fs-md);
1935    color: var(--color-text-light);
1936    line-height: 1.4;
1937}
1938
1939.gallery-card-image img {
1940    width: 100%;
1941    height: 100%;
1942    object-fit: cover;
1943    display: block;
1944}
1945
1946@media (max-width: 768px) {
1947    .gallery-card-image {
1948        display: none;
1949    }
1950}
1951
1952.gallery-body {
1953    grid-template-columns: repeat(2, minmax(0, 1fr));
1954    width: 100%;
1955    overflow: hidden;
1956    background-color: var(--color-white);
1957    display: grid;
1958    height: 100%;
1959}
1960
1961.gallery-body.active {
1962    display: grid !important;
1963}
1964
1965.gallery-body:hover .read-more svg {
1966    transform: translateX(4px);
1967    opacity: 1;
1968}
1969
1970@media (max-width: 768px) {
1971    .gallery-body {
1972        grid-template-columns: repeat(1, minmax(0, 1fr));
1973    }
1974}
1975
1976.selector-panels {
1977    max-width: 100%;
1978    width: 100%;
1979    display: grid;
1980    grid-template-areas: "slide";
1981}
1982
1983.selector-button p {
1984    text-align: center;
1985}
1986</style>
1987<style>
1988.feature {
1989    flex: 1;
1990    padding: var(--space-6);
1991    transition: all var(--transition-fast);
1992    display: flex;
1993    flex-direction: column;
1994    min-width: 200px;
1995}
1996
1997.feature-title {
1998    display: flex;
1999    align-items: center;
2000    gap: var(--space-3);
2001    font-weight: 600;
2002    font-size: var(--fs-md);
2003    margin-bottom: var(--space-6);
2004}
2005
2006.feature-description {
2007    font-size: var(--fs-base);
2008    line-height: 1.4;
2009    flex-grow: 1;
2010    display: flex;
2011    justify-content: center;
2012    align-items: flex-start;
2013    color: var(--color-text-light);
2014}
2015
2016.features-heading {
2017    gap: 70px;
2018    display: flex;
2019    flex-direction: column;
2020}
2021</style>
2022<style>
2023 summary {
2024    font-weight: bold;
2025    cursor: pointer;
2026    list-style: none;
2027    display: flex;
2028    align-items: center;
2029    justify-content: space-between;
2030}
2031
2032.accordion summary::-webkit-details-marker {
2033    display: none;
2034}
2035
2036.accordion summary::after {
2037    content: "▶";
2038    display: inline-block;
2039    margin-left: 0.5em;
2040    transition: transform 0.2s ease;
2041}
2042
2043details.accordion[open] summary::after {
2044    transform: rotate(90deg);
2045}
2046
2047details.accordion {
2048    border-bottom: 1px solid var(--color-border);
2049}
2050
2051</style>
2052<style>
2053
2054    @media (scripting: none) {
2055      #selector-input---verso-component-5-4:checked ~ .selector-list .selector-button[for="selector-input---verso-component-5-4"] {
2056        background-color: var(--color-primary);
2057        color: white;
2058      }
2059
2060      #--verso-component-5-panel-4 {
2061        display: none;
2062      }
2063
2064      #selector-input---verso-component-5-4:checked ~ .selector-panels > #--verso-component-5-panel-4 {
2065        display: block;
2066      }
2067    }
2068  
2069</style>
2070<style>
2071
2072    @media (scripting: none) {
2073      #selector-input---verso-component-28-0:checked ~ .selector-list .selector-button[for="selector-input---verso-component-28-0"] {
2074        background-color: var(--color-primary);
2075        color: white;
2076      }
2077
2078      #--verso-component-28-panel-0 {
2079        display: none;
2080      }
2081
2082      #selector-input---verso-component-28-0:checked ~ .selector-panels > #--verso-component-28-panel-0 {
2083        display: block;
2084      }
2085    }
2086  
2087</style>
2088<style>
2089#main-background {
2090    position: absolute;
2091    right: 0px;
2092    top: 0px;
2093}
2094
2095.background-wrapper {
2096    z-index: var(--z-below);
2097    width: min(1400px, 100vw);
2098}
2099
2100.background-wrapper svg {
2101    width: 100%;
2102    stroke: #D7E0E9;
2103}
2104
2105.dark-theme .background-wrapper svg {
2106    stroke: #1C1E26;
2107}
2108</style>
2109<style>
2110
2111    @media (scripting: none) {
2112      #selector-input---verso-component-28-2:checked ~ .selector-list .selector-button[for="selector-input---verso-component-28-2"] {
2113        background-color: var(--color-primary);
2114        color: white;
2115      }
2116
2117      #--verso-component-28-panel-2 {
2118        display: none;
2119      }
2120
2121      #selector-input---verso-component-28-2:checked ~ .selector-panels > #--verso-component-28-panel-2 {
2122        display: block;
2123      }
2124    }
2125  
2126</style>
2127<style>
2128
2129    @media (scripting: none) {
2130      #selector-input---verso-component-5-5:checked ~ .selector-list .selector-button[for="selector-input---verso-component-5-5"] {
2131        background-color: var(--color-primary);
2132        color: white;
2133      }
2134
2135      #--verso-component-5-panel-5 {
2136        display: none;
2137      }
2138
2139      #selector-input---verso-component-5-5:checked ~ .selector-panels > #--verso-component-5-panel-5 {
2140        display: block;
2141      }
2142    }
2143  
2144</style>
2145<style>
2146.selector-list {
2147    display: grid;
2148    grid-auto-flow: column;
2149    grid-auto-columns: 1fr;
2150    gap: var(--gap-sm);
2151    padding: var(--space-4);
2152    width: fit-content;
2153    position: relative;
2154    max-width: 100%;
2155    overflow-x: auto;
2156    box-sizing: border-box;
2157}
2158
2159@media (max-width: 768px) {
2160    .selector-list {
2161        width: 100%;
2162    }
2163}
2164
2165.selector-button {
2166    padding: var(--space-2) var(--space-6);
2167    border-radius: var(--radius-md);
2168    background: transparent;
2169    color: var(--color-text);
2170    border: none;
2171    cursor: pointer;
2172    font-weight: 500;
2173    font-size: var(--fs-base);
2174    position: relative;
2175    z-index: var(--z-above);
2176    transition: background var(--transition-fast), color var(--transition-fast);
2177    text-align: center;
2178    white-space: pre;
2179}
2180
2181.selector-button:hover {
2182    background: #7094de1c;
2183}
2184
2185.selector-button.active {
2186    color: var(--color-text-contrast);
2187}
2188
2189@media (scripting: none) {
2190    .selector-button.active {
2191        background-color: var(--color-primary);
2192    }
2193}
2194
2195.selector-group::before {
2196    content: '';
2197    position: absolute;
2198    top: 0;
2199    left: 0;
2200    width: 0;
2201    height: 100%;
2202    background: var(--color-primary-light);
2203    border-radius: var(--radius-md);
2204    transition: left var(--transition-base), width var(--transition-base);
2205    z-index: var(--z-normal);
2206}
2207
2208.selector-panel {
2209    display: none;
2210    width: 100%;
2211    min-width: 0;
2212}
2213
2214.selector-panel.active {
2215    display: block;
2216}
2217
2218.selector-panel.same-size {
2219    display: block;
2220    grid-area: slide;
2221    visibility: hidden;
2222    width: 100%;
2223}
2224
2225.selector-panel.same-size.active {
2226    visibility: visible;
2227}
2228
2229.selector-panel > article {
2230    height: 100%;
2231}
2232
2233.selectors-container {
2234    gap: var(--gap-lg);
2235    display: flex;
2236    align-items: center;
2237    flex-direction: column;
2238    max-width: 100vw;
2239}
2240
2241.active-background {
2242    position: absolute;
2243    height: 34px;
2244    background: var(--color-primary);
2245    border-radius: var(--radius-md);
2246    z-index: var(--z-normal);
2247}
2248</style>
2249<style>
2250
2251      .custom-subtitle {
2252        padding: 0px;
2253        font-size: 1.5rem !important;
2254        margin: 0px !important;
2255        border: none !important;
2256        font-weight: normal !important;
2257        color: #868686 !important;
2258        font-style: italic;
2259      }
2260
2261      @media (max-width: 768px) {
2262        .custom-subtitle {
2263          padding-top: 20px;
2264          font-size: 1.4rem !important;
2265        }
2266      }
2267    
2268</style>
2269<style>
2270.copy-button {
2271    position: absolute;
2272    top: 8px;
2273    right: 8px;
2274    padding: 6px 12px;
2275    font-size: 0.8em;
2276    cursor: pointer;
2277    z-index: 10;
2278    opacity: 0;
2279    transition: 0.2s opacity;
2280    border: 1px solid var(--color-border);
2281    background: var(--color-bg);
2282    border-radius: 5px;
2283    color: var(--color-text);
2284}
2285
2286.code-block-wrapper:hover .copy-button {
2287    opacity: 1;
2288}
2289
2290.hero .copy-button {
2291    right: 0px;
2292    top: 0px;
2293}
2294</style>
2295<style>
2296.hero {
2297    display: flex;
2298    flex-direction: column;
2299    justify-content: space-between;
2300    box-sizing: border-box;
2301    width: 100%;
2302    padding: 0;
2303    padding-top: var(--space-6);
2304}
2305
2306.hero-content {
2307    display: grid;
2308    gap: var(--space-8);
2309    align-items: center;
2310    flex-wrap: wrap;
2311    justify-content: space-between;
2312    margin: var(--space-4);
2313    grid-template-columns: 40% 50%;
2314}
2315
2316.hero-left {
2317    display: flex;
2318    flex-direction: column;
2319    width: 100%;
2320    justify-content: space-between;
2321}
2322
2323.hero-branding {
2324    display: flex;
2325    flex-direction: column;
2326    gap: var(--gap-lg);
2327    max-width: 100%;
2328}
2329
2330.hero-logo {
2331    width: 300px;
2332}
2333
2334.hero-tagline {
2335    margin-top: var(--space-2);
2336    font-size: var(--fs-md);
2337    color: var(--color-muted);
2338    line-height: 1.4;
2339    font-weight: 400;
2340}
2341
2342.hero-tagline span {
2343    color: var(--color-primary);
2344    font-weight: 500;
2345}
2346
2347.hero-buttons {
2348    display: flex;
2349    gap: var(--space-4);
2350    margin-top: var(--space-8);
2351    background-color: transparent;
2352}
2353
2354.hero-buttons a {
2355    width: 170px;
2356}
2357
2358.hero-buttons a.primary svg {
2359    fill: var(--color-text-contrast);
2360}
2361
2362.learn-button,
2363.install-button {
2364    position: relative;
2365}
2366
2367.learn-button span {
2368    position: relative;
2369    z-index: var(--z-above);
2370    display: flex;
2371    gap: var(--space-2);
2372    align-items: center;
2373}
2374
2375.learn-button span svg {
2376    transition: all var(--transition-base);
2377}
2378
2379.hero-right {
2380    position: relative;
2381}
2382
2383.hero-bottom {
2384    margin: var(--space-4);
2385    margin-top: var(--space-12);
2386    background-color: var(--color-white);
2387    border: 2px solid var(--color-primary);
2388    border-radius: var(--radius-lg);
2389    display: flex;
2390    box-shadow: 0px 35px 77px rgba(9, 62, 185, 0.10), 0px 140px 140px rgba(9, 62, 185, 0.09);
2391    justify-content: space-between;
2392    flex-wrap: wrap;
2393    box-shadow:
2394        0px 35px 77px rgba(9, 62, 185, 0.10),
2395        0px 140px 140px rgba(9, 62, 185, 0.09);
2396    padding: var(--space-6);
2397    box-sizing: border-box;
2398}
2399
2400.scroll-btn {
2401    position: absolute;
2402    background: rgb(0 0 0 / 10%);
2403    color: #ffffff;
2404    pointer-events: none;
2405    transition: opacity 0.3s ease;
2406    user-select: none;
2407    font-size: 1.2em;
2408    height: 100%;
2409    width: 50px;
2410    border: honeydew;
2411    border-radius: 0 !important;
2412    opacity: 0;
2413}
2414
2415.scroll-btn.right {
2416    right: 0;
2417}
2418
2419.code-gallery-content:hover .scroll-btn {
2420    opacity: 1;
2421    pointer-events: auto;
2422}
2423
2424.code-gallery-content * {
2425  overflow: auto;
2426}
2427
2428.hero-radial-blur {
2429    position: absolute;
2430    inset: 0;
2431    background: radial-gradient(farthest-side ellipse at center, #437ef78a 0%, rgba(255, 255, 255, 0) 80%);
2432    z-index: var(--z-below);
2433    width: 1000px;
2434    height: 1000px;
2435    left: calc((1070px - 600px) / 2 * -1);
2436    top: calc((900px - 500px) / 2 * -1);
2437    opacity: 60%;
2438    pointer-events: none;
2439}
2440
2441.projects-section {
2442    position: relative;
2443    overflow: visible;
2444}
2445
2446.projects-section .hero-radial-blur {
2447    left: 50%;
2448    top: 60%;
2449    transform: translate(-50%, -50%);
2450    width: 900px;
2451    height: 900px;
2452    opacity: 50%;
2453}
2454
2455.page-content {
2456    padding-top: 70px;
2457    display: flex;
2458    flex-direction: column;
2459    gap: var(--gap-xl);
2460    padding-bottom: var(--space-12);
2461}
2462
2463.read-more {
2464    font-weight: bold;
2465    text-transform: uppercase;
2466    font-size: var(--fs-sm);
2467    display: flex;
2468    align-items: center;
2469    gap: 5px;
2470    color: var(--color-text);
2471    margin-top: auto;
2472}
2473
2474.read-more svg {
2475    fill: var(--color-text) !important;
2476    transition: transform 0.2s, opacity 0.2s;
2477    opacity: 1;
2478}
2479
2480.read-more:hover svg {
2481    transform: translateX(4px);
2482    opacity: 1;
2483}
2484
2485.code-gallery-content .token, .code-gallery-content .inter-text {
2486    opacity: 0;
2487    animation: fadeInCode 0.3s ease forwards;
2488}
2489
2490@keyframes fadeIn {
2491    0% {
2492        opacity: 0;
2493        top: -20px;
2494    }
2495    100% {
2496        opacity: 1;
2497        top: 0;
2498    }
2499}
2500
2501@keyframes fadeInCode {
2502    0% {
2503        opacity: 0;
2504    }
2505    100% {
2506        opacity: 1;
2507    }
2508}
2509
2510@media (max-width: 1024px) {
2511    .hero-left {
2512        width: 100%;
2513    }
2514
2515    .code-gallery-box,
2516    .hero-right {
2517        width: 100%;
2518    }
2519
2520    .hero-content {
2521        display: flex;
2522        justify-content: center;
2523        padding: 20px;
2524    }
2525
2526    .hero-left {
2527        display: flex;
2528        align-items: center;
2529        flex-direction: row;
2530    }
2531
2532    .code-gallery-box,
2533    .hero-right {
2534        width: 100%;
2535    }
2536
2537    .hero-buttons a {
2538        padding: var(--space-4) var(--space-12);
2539    }
2540
2541    .hero-bottom {
2542        margin: var(--space-4);
2543        margin-top: var(--space-12);
2544    }
2545
2546    .hero-content {
2547        gap: 70px;
2548    }
2549
2550    .hero-buttons {
2551        display: flex;
2552        flex-direction: column;
2553        width: 100%;
2554        padding: 0 var(--gap-lg);
2555        box-sizing: border-box;
2556        margin: 0;
2557    }
2558
2559    .hero-buttons a {
2560        width: auto;
2561        height: 100%;
2562    }
2563
2564    .sponsors {
2565        width: calc(100% - var(--space-8)*2);
2566    }
2567}
2568
2569@media (max-width: 768px) {
2570    .hero {
2571        padding: var(--space-4);
2572        padding-top: var(--space-1);
2573        gap: 30px;
2574    }
2575
2576    .feature {
2577        min-width: auto;
2578        padding: var(--space-4);
2579    }
2580
2581    .hero-bottom {
2582        margin: 0px;
2583    }
2584
2585    .hero-tagline {
2586        text-align: center;
2587    }
2588
2589    .hero-left {
2590        width: 100%;
2591        flex-direction: column;
2592    }
2593
2594    .hero-radial-blur {
2595        display: none;
2596    }
2597
2598    .code-gallery-box,
2599    .hero-right {
2600        width: 100%;
2601        box-sizing: border-box;
2602    }
2603
2604    .hero-branding {
2605        display: flex;
2606        align-items: center;
2607    }
2608
2609    .hero-content {
2610        margin: 0px;
2611        justify-content: center;
2612        gap: 30px;
2613        padding: 0px;
2614        padding-top: 30px;
2615    }
2616
2617    .hero-buttons a {
2618        width: auto;
2619    }
2620
2621    .hero-buttons {
2622        flex-wrap: wrap;
2623        width: 100%;
2624        padding: 0;
2625        margin-top: 50px;
2626    }
2627
2628    .sponsors-content {
2629        justify-content: center;
2630        flex-direction: column;
2631        width: 100%;
2632    }
2633}
2634
2635#banner {
2636  background: var(--color-primary);
2637  color: var(--color-text-contrast);
2638  padding: 30px;
2639  text-align: center;
2640  text-transform: uppercase;
2641  margin-bottom: 20px;
2642}
2643
2644#banner a {
2645    color: var(--color-text-contrast);
2646    border-bottom: 1px solid var(--color-text-contrast);
2647}
2648
2649.hero-branding svg {
2650    max-width: 100%;
2651}
2652
2653.code-gallery-run {
2654    height: 40px;
2655    width: 40px;
2656    border: 2px solid #5185F4;
2657    box-sizing: border-box;
2658    display: flex;
2659    flex-shrink: 0;
2660    align-items: center;
2661    border-radius: 5px;
2662    justify-content: center;
2663    transition: background 0.2s;
2664}
2665
2666.code-gallery-run svg {
2667    transition: background 0.2s;
2668}
2669
2670.code-gallery-run:hover {
2671    background: #5185F4;
2672}
2673
2674.code-gallery-run:hover svg {
2675    fill: #ffffff;
2676}
2677
2678.code-gallery-tab {
2679    font-size: 0.85rem;
2680    font-weight: 500;
2681    color: var(--color-text-light);
2682}
2683
2684@media (max-width: 830px) {
2685    .hero-bottom {
2686        flex-direction: column;
2687    }
2688}
2689
2690#page {
2691    display: flex;
2692    flex-direction: column;
2693    padding-bottom: 100px;
2694    flex-grow: 1;
2695    gap: 100px;
2696    max-width: 100vw;
2697}
2698
2699@media (max-width: 768px) {
2700    #page {
2701        padding-top: 20px;
2702        gap: 50px;
2703    }
2704}
2705
2706.dark-theme:root .hero-branding svg {
2707    stroke: white;
2708}
2709</style>
2710<style>
2711.error-container {
2712    display: flex;
2713    flex-direction: row;
2714    gap: 4rem;
2715    align-items: center;
2716    justify-content: center;
2717    flex-wrap: wrap;
2718    padding: 150px;
2719    padding-top: 150px;
2720    padding-bottom: 50px;
2721    box-sizing: border-box;
2722}
2723
2724.error-container .image-section {
2725    flex: 1;
2726    display: flex;
2727    justify-content: center;
2728    align-items: center;
2729    min-width: 300px;
2730}
2731
2732.error-container .image-section img {
2733    width: min(400px, 100%);
2734    height: min(400px, 100%);
2735    max-width: 400px;
2736    max-height: 400px;
2737    display: flex;
2738    align-items: center;
2739    justify-content: center;
2740    text-align: center;
2741    box-sizing: border-box;
2742}
2743
2744.error-container .image-section img {
2745    width: min(400px, 100%);
2746    height: min(400px, 100%);
2747    max-width: 400px;
2748    max-height: 400px;
2749    display: flex;
2750    align-items: center;
2751    justify-content: center;
2752    text-align: center;
2753    box-sizing: border-box;
2754}
2755
2756.text-section {
2757    flex: 1;
2758    display: flex;
2759    flex-direction: column;
2760    gap: 1.25rem;
2761    padding: 1rem;
2762    min-width: 300px;
2763    max-width: 600px;
2764    text-align: center;
2765}
2766
2767.error-code {
2768    font-size: clamp(3rem, 8vw, 6rem);
2769    font-weight: bold;
2770    line-height: 1;
2771}
2772
2773.error-title {
2774    font-size: clamp(1.5rem, 4vw, 2rem);
2775    color: var(--color-text);
2776    line-height: 1.2;
2777    font-weight: bold;
2778    font-size: 2.3rem;
2779}
2780
2781.error-description {
2782    font-size: clamp(1rem, 2.5vw, 1.125rem);
2783    color: var(--color-text);
2784    line-height: 1.6;
2785    text-align: center;
2786}
2787
2788.action-buttons {
2789    margin-top: 1rem;
2790    display: flex;
2791    justify-content: center;
2792}
2793
2794
2795@media (max-width: 768px) {
2796    .error-container {
2797        flex-direction: column;
2798        gap: 1.5rem;
2799        padding: 2rem;
2800        padding-top: 3rem;
2801        text-align: center;
2802    }
2803
2804    .image-section,
2805    .text-section {
2806        flex: none;
2807        width: 100%;
2808        min-width: unset;
2809    }
2810
2811    .octopus-placeholder {
2812        width: min(300px, calc(100vw - 4rem), 40vw);
2813        height: min(300px, calc(100vw - 4rem), 40vw);
2814    }
2815
2816    .text-section {
2817        gap: 1rem;
2818        padding: 0px;
2819    }
2820}
2821
2822</style>
2823<style>
2824
2825    @media (scripting: none) {
2826      #selector-input---verso-component-5-3:checked ~ .selector-list .selector-button[for="selector-input---verso-component-5-3"] {
2827        background-color: var(--color-primary);
2828        color: white;
2829      }
2830
2831      #--verso-component-5-panel-3 {
2832        display: none;
2833      }
2834
2835      #selector-input---verso-component-5-3:checked ~ .selector-panels > #--verso-component-5-panel-3 {
2836        display: block;
2837      }
2838    }
2839  
2840</style>
2841<style>
2842.heading-section {
2843    text-align: center;
2844    display: flex;
2845    flex-direction: column;
2846    align-items: center;
2847    gap: var(--space-3);
2848    margin-bottom: var(--space-8);
2849}
2850
2851.heading-section > span {
2852    display: inline-flex;
2853    align-items: center;
2854    font-size: 0.72rem;
2855    font-weight: 700;
2856    letter-spacing: 0.13em;
2857    text-transform: uppercase;
2858    padding: 5px 16px;
2859    border-radius: var(--radius-pill);
2860    border: 1px solid transparent;
2861}
2862
2863/* Default / primary: solid primary colour pill, white text */
2864.heading-section > span.badge-primary {
2865    background: var(--color-primary);
2866    color: var(--color-text-contrast);
2867    border-color: transparent;
2868}
2869
2870/* Secondary: glassmorphic — for use on coloured/dark backgrounds */
2871.heading-section > span.badge-secondary {
2872    background: rgba(255, 255, 255, 0.12);
2873    color: rgba(255, 255, 255, 0.90);
2874    border-color: rgba(255, 255, 255, 0.22);
2875    backdrop-filter: blur(8px);
2876    -webkit-backdrop-filter: blur(8px);
2877}
2878
2879.heading-title {
2880    font-size: var(--fs-2xl);
2881    font-weight: 700;
2882    font-family: var(--font-primary);
2883    letter-spacing: -0.02em;
2884    line-height: 1.1;
2885    margin: var(--space-2) 0 0;
2886    color: var(--color-text);
2887    transition: color var(--transition-base);
2888}
2889
2890.heading-subtitle {
2891    font-size: var(--fs-md);
2892    color: var(--color-text-light);
2893    margin-top: var(--space-2);
2894    line-height: 1.55;
2895    transition: color var(--transition-base);
2896    max-width: 600px;
2897}
2898
2899.page-title {
2900    font-size: 2.5rem !important;
2901    margin-top: 4rem;
2902    font-weight: bold;
2903    text-align: left;
2904    padding: 0px !important;
2905    margin: 0px !important;
2906}
2907
2908@media (max-width: 768px) {
2909    .heading-title {
2910        font-size: 2rem;
2911    }
2912}
2913</style>
2914<style>
2915.no-js-warning {
2916    position: sticky;
2917    top: 0;
2918    width: 100%;
2919    background-color: red;
2920    color: white;
2921    text-align: center;
2922    padding: 0.75em;
2923    font-family: sans-serif;
2924    font-size: 1em;
2925    z-index: 9999;
2926}
2927</style>
2928<style>
2929.button-container {
2930    display: flex;
2931    gap: 10px;
2932    margin: 30px 0px;
2933}
2934
2935@media (max-width: 768px) {
2936    .button-container {
2937        flex-direction: column;
2938    }
2939}
2940
2941.btn {
2942    white-space: nowrap;
2943    display: flex;
2944    align-items: center;
2945    justify-content: center;
2946    gap: 5px;
2947    padding: 10px 30px;
2948    background-color: #3498db;
2949    color: white;
2950    border: none;
2951    border-radius: 5px;
2952    cursor: pointer;
2953    font-size: 16px;
2954    flex: 1;
2955    background: var(--card-bg) !important;
2956    border: 1px solid var(--color-border) !important;
2957    color: var(--color-text) !important;
2958    gap: 10px;
2959}
2960</style>
2961<style>
2962.modal-backdrop {
2963    max-height: 100vh;
2964    position: fixed;
2965    top: 0;
2966    left: 0;
2967    width: 100vw;
2968    height: 100vh;
2969    background-color: rgba(0, 0, 0, 0.75);
2970    display: flex;
2971    align-items: center;
2972    justify-content: center;
2973    z-index: 9999;
2974}
2975
2976.modal {
2977    background: var(--color-white);
2978    padding: 2rem;
2979    border-radius: 0.5rem;
2980    max-width: 500px;
2981    width: 90%;
2982    position: relative;
2983    box-shadow: 0 2px 10px rgba(0, 0, 0, 0.2);
2984    max-height: calc(100vh - 40px);
2985    box-sizing: border-box;
2986    overflow: auto;
2987    display: flex;
2988    flex-wrap: wrap;
2989    width: 100%;
2990    transform-origin: center;
2991    will-change: transform, opacity;
2992}
2993
2994.modal-close {
2995    color: var(--color-text);
2996    position: absolute;
2997    top: 0.5rem;
2998    right: 0.75rem;
2999    background: none;
3000    border: none;
3001    font-size: 1.5rem;
3002    cursor: pointer;
3003}
3004
3005.hidden {
3006    display: none;
3007}
3008
3009body.modal-open {
3010    overflow: hidden;
3011}
3012
3013/* Modal for Step 2 */
3014
3015.modal-content {
3016  padding: 2rem;
3017  border-radius: 1rem;
3018}
3019
3020.modal-content h2 {
3021  font-size: 1.5rem;
3022  margin-bottom: 0.5rem;
3023  font-weight: 600;
3024  padding-left: 0.5rem;
3025  text-align: center;
3026  margin: 0px !important; 
3027}
3028
3029.steps {
3030  display: flex;
3031  flex-direction: column;
3032  gap: 2rem;
3033  margin-top: 2rem;
3034}
3035
3036.step .screenshot, .step .gallery-item {
3037    width: 120px;
3038}
3039
3040.step {
3041  display: flex;
3042  gap: 1rem;
3043  align-items: center;
3044  transition: transform 0.2s ease-in-out;
3045}
3046
3047.step img {
3048  width: 120px !important;
3049  height: 120px !important;
3050  object-fit: cover;
3051  border-radius: 0.5rem;
3052  border: 1px solid #444;
3053  margin: 0px;
3054}
3055
3056.step p {
3057  margin: 0;
3058  font-size: 1rem;
3059  line-height: 1.4;
3060}
3061
3062.modal-content a {
3063    text-align: center;
3064    width: 100%;
3065    padding-top: 20px;
3066    box-sizing: border-box;
3067    display: block;
3068    background: none !important;
3069    border: none !important;
3070}
3071
3072@media (max-width: 768px) {
3073  .modal {
3074    border-radius: 0px;
3075  }
3076}
3077</style>
3078<style>
3079
3080    @media (scripting: none) {
3081      #selector-input---verso-component-28-1:checked ~ .selector-list .selector-button[for="selector-input---verso-component-28-1"] {
3082        background-color: var(--color-primary);
3083        color: white;
3084      }
3085
3086      #--verso-component-28-panel-1 {
3087        display: none;
3088      }
3089
3090      #selector-input---verso-component-28-1:checked ~ .selector-panels > #--verso-component-28-panel-1 {
3091        display: block;
3092      }
3093    }
3094  
3095</style>
3096<script>
3097      
3098document.addEventListener('DOMContentLoaded', () => {
3099    initTabSelectors();
3100    initAccessibilityTab();
3101
3102    const shouldChangeDefault = detectOS() && document.querySelector('.device-tabs');
3103    if (shouldChangeDefault) {
3104        changeTabDefault();
3105    }
3106
3107    tippy('.code-gallery-run', {
3108        content: "Opens the current code in the playground!",
3109    });
3110
3111    tippy('.social-icon', {
3112        placement: 'top',
3113    });
3114
3115});
3116
3117function observeUntilVisible(element, callback) {
3118    if (!element) return;
3119
3120    const observers = [];
3121
3122    function isElementVisible(el) {
3123        while (el) {
3124            const style = getComputedStyle(el);
3125            if (style.display === 'none' || style.visibility === 'hidden' || style.opacity === '0') {
3126                return false;
3127            }
3128            el = el.parentElement;
3129        }
3130        return true;
3131    }
3132
3133    function disconnectAllObservers(observerList) {
3134        observerList.forEach(observer => observer.disconnect());
3135    }
3136
3137    const targetObserver = new MutationObserver(() => {
3138        if (isElementVisible(element)) {
3139            callback();
3140            disconnectAllObservers(observers);
3141        }
3142    });
3143
3144    targetObserver.observe(element, {
3145        attributes: true,
3146        attributeFilter: ['style', 'class']
3147    });
3148    observers.push(targetObserver);
3149
3150    let parent = element.parentElement;
3151    while (parent && parent !== document.body) {
3152        const parentObserver = new MutationObserver(() => {
3153            if (isElementVisible(element)) {
3154                callback();
3155                disconnectAllObservers(observers);
3156            }
3157        });
3158
3159        parentObserver.observe(parent, {
3160            attributes: true,
3161            attributeFilter: ['style', 'class']
3162        });
3163        observers.push(parentObserver);
3164
3165        parent = parent.parentElement;
3166    }
3167
3168    if (isElementVisible(element)) {
3169        callback();
3170        disconnectAllObservers(observers);
3171    }
3172}
3173
3174function getHiddenElementRect(element) {
3175    const clone = element.cloneNode(true);
3176
3177    clone.style.position = 'absolute';
3178    clone.style.visibility = 'hidden';
3179    clone.style.display = 'block';
3180    clone.style.top = '-9999px';
3181    document.body.appendChild(clone);
3182
3183    const rect = clone.getBoundingClientRect();
3184    document.body.removeChild(clone);
3185
3186    return rect;
3187}
3188
3189function initAccessibilityTab() {
3190    document.querySelectorAll(".selector-button").forEach(button => {
3191        button.addEventListener('keydown', (e) => {
3192            if (e.key === 'Enter') {
3193                e.preventDefault();
3194                button.click();
3195            }
3196        });
3197    });
3198}
3199
3200function activateTab(button, contentContainer, activeState) {
3201    const {
3202        activeButton,
3203        activePanel
3204    } = activeState;
3205
3206    if (button === activeButton) return;
3207
3208    if (activeButton) {
3209        activeButton.classList.remove('active');
3210        activeButton.setAttribute('aria-selected', 'false');
3211    }
3212
3213    button.classList.add('active');
3214    button.setAttribute('aria-selected', 'true');
3215    activeState.activeButton = button;
3216
3217    const targetPanel = contentContainer.querySelector(`:scope > .selector-panel[data-id="${button.dataset.id}"]`);
3218
3219    if (activePanel && activePanel !== targetPanel) {
3220        activePanel.classList.remove('active');
3221        activePanel.setAttribute('aria-hidden', 'true');
3222    }
3223
3224    if (targetPanel) {
3225        targetPanel.classList.add('active');
3226        targetPanel.setAttribute('aria-hidden', 'false');
3227        activeState.activePanel = targetPanel;
3228    }
3229}
3230
3231function setActiveTabByIndex(tabsContainer, index) {
3232    const tabButtons = tabsContainer.querySelectorAll(':scope > .selector-list > .selector-button');
3233    if (tabButtons.length === 0 || index < 0 || index >= tabButtons.length) return;
3234
3235    const button = tabButtons[index];
3236
3237    const dataId = tabsContainer.dataset.id;
3238    const contentContainer = document.querySelector(`.selector-panels[data-id="${dataId}"]`);
3239    if (!contentContainer) return;
3240
3241    let activeButton = tabsContainer.querySelector(':scope > .selector-list > .selector-button.active');
3242    let activePanel = contentContainer.querySelector(':scope > .selector-panel.active');
3243    const activeState = {
3244        activeButton,
3245        activePanel
3246    };
3247
3248    activateTab(button, contentContainer, activeState);
3249
3250    const tabList = tabsContainer.querySelector('.selector-list');
3251    if (tabList) {
3252        requestAnimationFrame(() => {
3253            requestAnimationFrame(() => {
3254                updateTabBackgroundIndicator(tabList, button);
3255            });
3256        });
3257    }
3258}
3259
3260function initTabContentPanels(tabsContainer, contentContainer) {
3261    const tabButtons = tabsContainer.querySelectorAll(':scope > .selector-list > .selector-button');
3262
3263    if (tabButtons.length === 0) return;
3264
3265    let initialButton = tabsContainer.querySelector(':scope > .selector-list > .selector-button[data-initial="true"]');
3266    if (initialButton) {
3267        initialButton.classList.add('active');
3268    }
3269
3270    let activeButton = tabsContainer.querySelector(':scope > .selector-list > .selector-button.active');
3271    let activePanel = contentContainer.querySelector(':scope > .selector-panel.active');
3272
3273    const activeState = {
3274        activeButton,
3275        activePanel
3276    };
3277
3278    tabButtons.forEach(button => {
3279        button.setAttribute('role', 'tab');
3280        button.setAttribute('aria-selected', button === activeButton ? 'true' : 'false');
3281
3282        button.addEventListener('click', () => {
3283            activateTab(button, contentContainer, activeState);
3284        });
3285    });
3286}
3287
3288function setBackgroundPosition(activeBackground, tab) {
3289    tab.offsetHeight; // force reflow
3290    activeBackground.style.left = `${tab.offsetLeft}px`;
3291    activeBackground.style.top = `${tab.offsetTop}px`;
3292    activeBackground.style.width = `${tab.offsetWidth}px`;
3293    activeBackground.style.height = `${tab.offsetHeight}px`;
3294}
3295
3296function springBackgroundPosition(activeBackground, tab) {
3297    const animate = window.Motion?.animate;
3298    if (!animate) {
3299        setBackgroundPosition(activeBackground, tab);
3300        return;
3301    }
3302    animate(
3303        activeBackground,
3304        { left: tab.offsetLeft, top: tab.offsetTop, width: tab.offsetWidth, height: tab.offsetHeight },
3305        { type: 'spring', stiffness: 400, damping: 28 }
3306    );
3307}
3308
3309function updateTabBackgroundIndicator(tabGroup, activeTab) {
3310    const activeBackground = tabGroup.querySelector('.active-background');
3311    if (!activeBackground || !activeTab) return;
3312
3313    activeBackground.style.opacity = '1';
3314
3315    if ((activeTab.offsetLeft === 0 || activeTab.offsetWidth === 0)) {
3316        observeUntilVisible(activeTab, () => setBackgroundPosition(activeBackground, activeTab));
3317        return;
3318    }
3319
3320    setBackgroundPosition(activeBackground, activeTab);
3321}
3322
3323function initTabBackgroundIndicator(tabGroup) {
3324    const tabButtons = tabGroup.querySelectorAll(':scope > .selector-button');
3325    if (tabButtons.length === 0) return;
3326
3327    const activeBackground = document.createElement('div');
3328    activeBackground.classList.add('active-background');
3329    tabGroup.appendChild(activeBackground);
3330
3331    let initialized = false;
3332
3333    function positionBackground(tab, instant = false) {
3334        if (tab.offsetLeft === 0 && !instant) {
3335            observeUntilVisible(tab, () => positionBackground(tab, true));
3336            return;
3337        }
3338        if (!initialized || instant) {
3339            setBackgroundPosition(activeBackground, tab);
3340            initialized = true;
3341        } else {
3342            springBackgroundPosition(activeBackground, tab);
3343        }
3344    }
3345
3346    let activeTab = tabGroup.querySelector(':scope > .selector-button.active');
3347
3348    window.addEventListener('resize', () => {
3349        if (activeTab) positionBackground(activeTab, true);
3350    });
3351
3352    tabButtons.forEach(tab => {
3353        tab.addEventListener('click', () => {
3354            tabButtons.forEach(button => {
3355                button.classList.remove('active');
3356                button.setAttribute('aria-selected', 'false');
3357            });
3358
3359            activeTab = tab;
3360            tab.classList.add('active');
3361            tab.setAttribute('aria-selected', 'true');
3362
3363            requestAnimationFrame(() => positionBackground(tab));
3364        });
3365    });
3366
3367    const isDeviceTabs = tabGroup.closest('.device-tabs');
3368    const shouldChangeDefault = isDeviceTabs && detectOS();
3369
3370    if (shouldChangeDefault) {
3371        activeBackground.style.opacity = '0';
3372    } else if (activeTab) {
3373        positionBackground(activeTab);
3374    }
3375}
3376
3377function initTabSelectors() {
3378    const tabContainers = document.querySelectorAll('.selectors-container');
3379    if (tabContainers.length === 0) return;
3380
3381    tabContainers.forEach((container) => {
3382        const tabList = container.querySelector('.selector-list');
3383        if (!tabList) return;
3384
3385        const dataId = container.dataset.id;
3386        const panelsContainer = document.querySelector(`.selector-panels[data-id="${dataId}"]`);
3387
3388        if (panelsContainer) {
3389            initTabContentPanels(container, panelsContainer);
3390        }
3391
3392        initTabBackgroundIndicator(tabList);
3393    });
3394}
3395
3396function detectOS() {
3397    const platform = navigator.platform.toLowerCase();
3398
3399    if (platform.includes('win')) {
3400        return 3;
3401    } else if (platform.includes('mac')) {
3402        return 2;
3403    } else if (platform.includes('linux')) {
3404        return 1;
3405    } else {
3406        return 0;
3407    }
3408}
3409
3410function changeTabDefault() {
3411    let os = detectOS();
3412
3413    if (os) {
3414        const osTabButton = document.querySelector(`.device-tabs`);
3415
3416        if (osTabButton) {
3417            setActiveTabByIndex(osTabButton, os - 1);
3418        }
3419    }
3420}
3421</script>
3421
3422    
3423<script>
3424      
3425let _animate = null;
3426
3427async function getAnimate() {
3428    if (_animate) return _animate;
3429    const { animate } = await import('https://cdn.jsdelivr.net/npm/motion@latest/+esm');
3430    _animate = animate;
3431    return animate;
3432}
3433
3434async function openModal(id) {
3435    const backdrop = document.getElementById(id);
3436    if (!backdrop) return;
3437
3438    const modal = backdrop.querySelector('.modal');
3439    backdrop.classList.remove('hidden');
3440    document.body.classList.add('modal-open');
3441
3442    const animate = await getAnimate();
3443    animate(backdrop, { opacity: [0, 1] }, { duration: 0.2, easing: 'ease-out' });
3444    animate(modal, { opacity: [0, 1], scale: [0.95, 1] }, { duration: 0.25, easing: [0.34, 1.56, 0.64, 1] });
3445}
3446
3447async function closeModal(backdrop) {
3448    const modal = backdrop.querySelector('.modal');
3449    const animate = await getAnimate();
3450
3451    animate(modal, { opacity: 0, scale: 0.95 }, { duration: 0.15, easing: 'ease-in' });
3452    await animate(backdrop, { opacity: 0 }, { duration: 0.2, easing: 'ease-in' });
3453
3454    backdrop.classList.add('hidden');
3455    document.body.classList.remove('modal-open');
3456}
3457
3458document.addEventListener('DOMContentLoaded', () => {
3459    getAnimate();
3460    registerModals();
3461});
3462
3463function registerModals() {
3464    document.querySelectorAll('[data-modal-target]').forEach(trigger => {
3465        trigger.addEventListener('click', () => {
3466            const targetId = trigger.getAttribute('data-modal-target');
3467            if (targetId) openModal(targetId);
3468        });
3469    });
3470
3471    document.querySelectorAll('.modal-backdrop').forEach(backdrop => {
3472        document.body.appendChild(backdrop);
3473
3474        backdrop.addEventListener('click', (e) => {
3475            const modalBox = backdrop.querySelector('.modal');
3476            if (!modalBox.contains(e.target) || e.target.classList.contains('modal-close')) {
3477                closeModal(backdrop);
3478            }
3479        });
3480    });
3481}
3482
3483</script>
3483
3484    
3485<script>
3486      
3487document.addEventListener('DOMContentLoaded', () => {
3488    initCodeTabs();
3489    removeTabFocus();
3490});
3491
3492function removeTabFocus() {
3493    const container = document.querySelector('.hero-right');
3494
3495    if (container) {
3496        container.querySelectorAll('a, button, input, textarea, select, [tabindex]')
3497            .forEach(el => el.setAttribute('tabindex', '-1'));
3498    }
3499}
3500
3501function initCodeTabs() {
3502    const tabs = Array.from(document.querySelectorAll('.code-gallery-tab')).filter(tab => !tab.classList.contains('filler'));
3503    const codeSnippets = document.querySelectorAll('.code-gallery-snippet');
3504    const codeTips = document.querySelectorAll('.code-gallery-tip');
3505    const border = document.querySelector('.code-gallery-tab-border');
3506    const nextButton = document.querySelector('.hero-footer-next');
3507
3508    if (tabs.length === 0 || !border) return;
3509
3510    let activeIndex = tabs.findIndex(tab => tab.classList.contains('active'));
3511    if (activeIndex === -1) activeIndex = 0;
3512
3513    function updateBorder(tab) {
3514        const tabRect = tab.getBoundingClientRect();
3515        const parentRect = tab.parentElement.getBoundingClientRect();
3516        const parentScrollLeft = tab.parentElement.scrollLeft || 0;
3517
3518        border.style.left = `${tabRect.left - parentRect.left + parentScrollLeft}px`;
3519        border.style.width = `${tabRect.width}px`;
3520    }
3521
3522    function setActiveCodeTab(index) {
3523        tabs.forEach((tab, i) => {
3524            const isActive = i === index;
3525            tab.classList.toggle('active', isActive);
3526            tab.setAttribute('aria-selected', isActive ? 'true' : 'false');
3527        });
3528
3529        codeSnippets.forEach((snippet, i) => {
3530            snippet.classList.toggle('visible-code', i === index);
3531            snippet.setAttribute('aria-hidden', i !== index);
3532        });
3533
3534        codeTips.forEach((tip, i) => {
3535            tip.classList.toggle('active', i === index);
3536            tip.setAttribute('aria-hidden', i !== index);
3537        });
3538
3539        updateBorder(tabs[index]);
3540        activeIndex = index;
3541    }
3542
3543    tabs.forEach((tab, index) => {
3544        tab.setAttribute('role', 'tab');
3545        tab.setAttribute('aria-selected', index === activeIndex ? 'true' : 'false');
3546
3547        tab.addEventListener('click', () => {
3548            setActiveCodeTab(index);
3549        });
3550    });
3551
3552    // Listen for scroll events on the tab container to update border position
3553    const tabContainer = tabs[0]?.parentElement;
3554    if (tabContainer) {
3555        tabContainer.addEventListener('scroll', () => {
3556            updateBorder(tabs[activeIndex]);
3557        });
3558    }
3559
3560    if (nextButton) {
3561        nextButton.addEventListener('click', () => {
3562            setActiveCodeTab((activeIndex + 1) % tabs.length);
3563        });
3564    }
3565
3566    setActiveCodeTab(activeIndex);
3567}
3568
3569function initCodeAnimations() {
3570    const codeSnippets = document.querySelectorAll('.code-gallery-snippet');
3571
3572    codeSnippets.forEach(snippet => {
3573        const tokens = snippet.querySelectorAll('.token, .inter-text');
3574
3575        tokens.forEach((token, i) => {
3576            token.style.animationDelay = `${i * 3 + 30}ms`;
3577        });
3578    });
3579}
3580</script>
3580
3581    
3582<meta name="viewport" content="width=device-width, initial-scale=1">
3583    <title>About — Lean Lang </title><meta name="description" content="Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code.">
3584    <link rel="icon" href="https://lean-lang.org/static/favicon-light.ico">
3585    <link rel="apple-touch-icon" href="https://lean-lang.org/static/apple-touch-icon.png">
3586    <meta name="theme-color" content="#3D6AC9">
3587    <meta property="og:title" content="Lean Programming Language">
3588    <meta property="og:type" content="article">
3589    <meta property="og:image" content="https://lean-lang.org/static/png/banner.png">
3590    <meta property="og:url" content="https://lean-lang.org">
3591    <meta property="og:image:alt" content="Lean Programming Language">
3592    <meta property="og:site_name" content="Lean Language">
3593    <meta name="twitter:title" content="Lean Programming Language">
3594    <meta name="twitter:description" content="Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code.">
3595    <meta name="twitter:image" content="https://lean-lang.org/static/png/banner.png">
3596    <meta name="twitter:image:alt" content="Lean Programming Language">
3597    <meta name="twitter:creator" content="@leanprover">
3598    <meta name="twitter:card" content="summary_large_image">
3599    <link rel="preconnect" href="https://fonts.googleapis.com">
3600    <link rel="preconnect" href="https://fonts.gstatic.com" crossorigin="anonymous">
3601    <link rel="stylesheet" href="https://fonts.googleapis.com/css2?family=Fira+Code:[email protected]&amp;
3601family=Open+Sans:ital,wght@0,300..800;1,300..800&amp;family=Oranienbaum&amp;display=swap">
3602    <style>/* Base Variables */
3603:root {
3604    --font-primary: 'Open Sans', Arial, sans-serif;
3605    --font-secondary: 'Oranienbaum', serif;
3606    --fs-xs: 0.75rem;
3607    --fs-sm: 0.875rem;
3608    --fs-base: 1rem;
3609    --fs-md: 17px;
3610    --fs-lg: 1.25rem;
3611    --fs-xl: 2rem;
3612    --fs-2xl: 3.3rem;
3613    --space-1: 0.25rem;
3614    --space-2: 0.5rem;
3615    --space-3: 0.75rem;
3616    --space-4: 1rem;
3617    --space-5: 1.25rem;
3618    --space-6: 1.5rem;
3619    --space-8: 2rem;
3620    --space-10: 2.5rem;
3621    --space-12: 3rem;
3622    --space-13: 3.5rem;
3623    --space-14: 4rem;
3624    --space-16: 5rem;
3625    --gap-sm: var(--space-2);
3626    --gap-md: 10px;
3627    --gap-lg: 30px;
3628    --gap-xl: 100px;
3629    --section-padding: var(--space-10);
3630    --section-padding-top: var(--space-16);
3631    --radius-sm: 0.25rem;
3632    --radius-md: 0.5rem;
3633    --radius-lg: 1rem;
3634    --radius-pill: 9999px;
3635    --container-width: 1240px;
3636    --logo-size: 1.25rem;
3637    --logo-footer-size: 60px;
3638    --icon-size: 64px;
3639    --nav-padding-y: var(--space-6);
3640    --nav-padding-x: 10vw;
3641    --nav-height: calc(var(--nav-padding-y) * 2 + 2em);
3642    --transition-fast: 0.2s;
3643    --transition-base: 0.3s;
3644    --transition-slow: 0.6s;
3645    --transition-delay-none: 0s;
3646    --transition-delay-small: 0.05s;
3647    --transition-delay-medium: 0.1s;
3648    --transition-delay-large: 0.15s;
3649    --animation-delay: 10000ms;
3650    --z-below: -1;
3651    --z-normal: 0;
3652    --z-above: 1;
3653    --z-header: 1000;
3654    --color-surface: #fff;
3655    --color-primary: #386EE0;
3656    --color-primary-focus: #1D4ED8;
3657    --color-primary-light: #4a90e2;
3658    --color-secondary: #607D8B;
3659    --color-text: #333;
3660    --color-text-contrast: white;
3661    --color-text-light: #64748b;
3662    --color-muted: #607D8B;
3663    --color-bg: #F9FBFD;
3664    --color-bg-translucent: rgba(249, 251, 253, 0.81);
3665    --color-white: #fff;
3666    --color-border: #E4EBF3;
3667    --color-border-nav: #E4EBF3;
3668    --color-border-light: #D1D9E2;
3669    --color-hover: rgba(56, 110, 224, 0.08);
3670    --color-link-hover: #0073e6;
3671    --color-shadow: rgba(35, 55, 139, 0.1);
3672    --btn-bg: var(--color-primary);
3673    --btn-text: var(--color-white);
3674    --btn-font: var(--font-primary);
3675    --btn-radius: var(--radius-md);
3676    --card-bg: var(--color-white);
3677    --card-border: var(--color-border-light);
3678    --testimonial-bg: var(--color-primary);
3679    --testimonial-text: var(--color-white);
3680}
3681
3682/* Dark Theme */
3683.dark-theme {
3684    --color-surface: #121212;
3685    --color-primary: #3b94ff;
3686    --color-primary-focus: #669df6;
3687    --color-primary-light: #6aadfe;
3688    --color-secondary: #aabfc9;
3689    --color-text: #eee;
3690    --color-text-light: #bbb;
3691    --color-text-contrast: white;
3692    --color-muted: #90a4ae;
3693    --color-bg: #181818;
3694    --color-bg-translucent: rgba(24, 24, 24, 0.85);
3695    --color-white: #1e1e1e;
3696    --color-border: #333;
3697    --color-border-nav: #333;
3698    --color-border-light: #444;
3699    --color-hover: rgba(255, 255, 255, 0.08);
3700    --color-link-hover: #4d9efc;
3701    --color-shadow: rgba(0, 0, 0, 0.5);
3702    --btn-bg: var(--color-primary);
3703    --btn-text: var(--color-white);
3704    --card-bg: #1f1f1f;
3705    --card-border: #2a2a2a;
3706    --testimonial-bg: #2e3a59;
3707    --testimonial-text: #fff;
3708}</style><link rel="apple-touch-icon" href="apple-touch-icon.png">
3709    
3709<script async="" src="https://plausible.io/js/pa-RTua_4FfKHhfAvAc3liZd.js"></script>
3709
3710    
3710<script>
3711      window.plausible=window.plausible||function(){(plausible.q=plausible.q||[]).push(arguments)},plausible.init=plausible.init||function(i){plausible.o=i||{}};
3712        plausible.init()</script>
3712
3713    </head>
3714  <body>
3715    <noscript><div class="no-js-warning">
3716        If you want the full website experience, enable JS</div>
3717      </noscript><header class="site-header">
3718      <nav class="navbar" role="navigation" aria-label="Primary navigation">
3719        <div class="navbar-container container">
3720          <a class="nav-logo" href="/"><svg width="70" height="20" viewBox="0 0 486 169" xmlns="http://www.w3.org/2000/svg" stroke="#386EE0" fill="transparent" stroke-width="10"><path d="M206.333 5.67949H105.667M206.333 5.67949L243.25 84.5M206.333 5.67949V84.5M243.25 84.5H317.549M243.25 84.5L279.667 163.321L280.889 163.318L317.549 84.5M206.333 84.5V163.321H5V5M206.333 84.5H105.667M317.549 84.5L353 5.67949M353 5.67949V164M353 5.67949H353.667L480.333 163.454H481V5" stroke-linecap="round" stroke-linejoin="round"></path></svg></a><div class="nav-toggle">
3721            <input type="checkbox" id="nav-toggle" class="nav-toggle-checkbox"><label for="nav-toggle" class="nav-toggle-label" aria-label="Toggle navigation menu">☰</label></div>
3722          <menu class="desktop-menu"><ul class="desktop-menu-part">
3723              <li class="nav-item">
3724                <a href="/install" class="nav-link" aria-label="" target="_self">Install</a></li>
3725              <li class="nav-item">
3726                <a href="/learn" class="nav-link" aria-label="" target="_self">Learn</a></li>
3727              <li class="nav-item">
3728                <a href="/community" class="nav-link" aria-label="" target="_self">Community</a></li>
3729              <li class="nav-item">
3730                <a href="/use-cases" class="nav-link" aria-label="" target="_self">Use Cases</a></li>
3731              <li class="nav-item nav-group">
3732                <a href="/fro" class="nav-link nav-group-label" aria-label="FRO">FRO</a><ul class="nav-group-items"></ul>
3733                </li>
3734              <li class="nav-item nav-divider" aria-hidden="true">
3735                <span class="divider"></span></li>
3736              <li class="nav-item">
3737                <a href="https://live.lean-lang.org/?from=lean" class="nav-link" aria-label="" target="_blank">Playground</a></li>
3738              <li class="nav-item">
3739                <a href="https://leanprover-community.github.io/" class="nav-link" aria-label="" target="_blank">Mathlib</a></li>
3740              <li class="nav-item">
3741                <a href="https://www.cslib.io/" class="nav-link" aria-label="" target="_blank">CSLib</a></li>
3742              <li class="nav-item">
3743                <a href="https://reservoir.lean-lang.org/" class="nav-link" aria-label="" target="_blank">Reservoir</a></li>
3744              </ul>
3745            <ul class="desktop-menu-part">
3746              <li class="nav-item">
3747                <button class="nav-link change-theme" aria-label="Change Theme"><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24" width="25" height="25"><g data-name="Layer 2"><g data-name="moon"><rect width="24" height="24" opacity="0"></rect><path d="M12.3 22h-.1a10.31 10.31 0 0 1-7.34-3.15 10.46 10.46 0 0 1-.26-14 10.13 10.13 0 0 1 4-2.74 1 1 0 0 1 1.06.22 1 1 0 0 1 .24 1 8.4 8.4 0 0 0 1.94 8.81 8.47 8.47 0 0 0 8.83 1.94 1 1 0 0 1 1.27 1.29A10.16 10.16 0 0 1 19.6 19a10.28 10.28 0 0 1-7.3 3zM7.46 4.92a7.93 7.93 0 0 0-1.37 1.22 8.44 8.44 0 0 0 .2 11.32A8.29 8.29 0 0 0 12.22 20h.08a8.34 8.34 0 0 0 6.78-3.49A10.37 10.37 0 0 1 7.46 4.92z"></path></g></g></svg></button></li>
3748              <li class="nav-item">
3749                <a href="https://github.com/leanprover/lean4" class="nav-link" aria-label="Github" target="_blank"><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24" width="25" height="25"><g data-name="Layer 2"><rect width="24" height="24" opacity="0"></rect><path d="M16.24 22a1 1 0 0 1-1-1v-2.6a2.15 2.15 0 0 0-.54-1.66 1 1 0 0 1 .61-1.67C17.75 14.78 20 14 20 9.77a4 4 0 0 0-.67-2.22 2.75 2.75 0 0 1-.41-2.06 3.71 3.71 0 0 0 0-1.41 7.65 7.65 0 0 0-2.09 1.09 1 1 0 0 1-.84.15 10.15 10.15 0 0 0-5.52 0 1 1 0 0 1-.84-.15 7.4 7.4 0 0 0-2.11-1.09 3.52 3.52 0 0 0 0 1.41 2.84 2.84 0 0 1-.43 2.08 4.07 4.07 0 0 0-.67 2.23c0 3.89 1.88 4.93 4.7 5.29a1 1 0 0 1 .82.66 1 1 0 0 1-.21 1 2.06 2.06 0 0 0-.55 1.56V21a1 1 0 0 1-2 0v-.57a6 6 0 0 1-5.27-2.09 3.9 3.9 0 0 0-1.16-.88 1 1 0 1 1 .5-1.94 4.93 4.93 0 0 1 2 1.36c1 1 2 1.88 3.9 1.52a3.89 3.89 0 0 1 .23-1.58c-2.06-.52-5-2-5-7a6 6 0 0 1 1-3.33.85.85 0 0 0 .13-.62 5.69 5.69 0 0 1 .33-3.21 1 1 0 0 1 .63-.57c.34-.1 1.56-.3 3.87 1.2a12.16 12.16 0 0 1 5.69 0c2.31-1.5 3.53-1.31 3.86-1.2a1 1 0 0 1 .63.57 5.71 5.71 0 0 1 .33 3.22.75.75 0 0 0 .11.57 6 6 0 0 1 1 3.34c0 5.07-2.92 6.54-5 7a4.28 4.28 0 0 1 .22 1.67V21a1 1 0 0 1-.94 1z"></path></g></svg></a></li>
3750              </ul>
3751            </menu></div>
3752        <menu class="mobile-nav"><ul class="nav-list">
3753            <li class="nav-item">
3754              <a href="/install" class="nav-link" aria-label="" target="_self">Install</a></li>
3755            <li class="nav-item">
3756              <a href="/learn" class="nav-link" aria-label="" target="_self">Learn</a></li>
3757            <li class="nav-item">
3758              <a href="/community" class="nav-link" aria-label="" target="_self">Community</a></li>
3759            <li class="nav-item">
3760              <a href="/use-cases" class="nav-link" aria-label="" target="_self">Use Cases</a></li>
3761            <li class="nav-item">
3762              <a href="https://live.lean-lang.org/?from=lean" class="nav-link" aria-label="" target="_blank">Playground</a></li>
3763            <li class="nav-item">
3764              <a href="https://leanprover-community.github.io/" class="nav-link" aria-label="" target="_blank">Mathlib</a></li>
3765            <li class="nav-item">
3766              <a href="https://www.cslib.io/" class="nav-link" aria-label="" target="_blank">CSLib</a></li>
3767            <li class="nav-item">
3768              <a href="https://reservoir.lean-lang.org/" class="nav-link" aria-label="" target="_blank">Reservoir</a></li>
3769            <li class="nav-item has-submenu">
3770              <input type="checkbox" id="mobile-group-FRO-1710831059350241967" class="mobile-group-toggle" hidden="true"><label for="mobile-group-FRO-1710831059350241967" class="nav-link" aria-label="Toggle FRO navigation menu">FRO</label><ul class="submenu">
3771                <li class="nav-item">
3772                  <a href="/fro" class="nav-link" aria-label="FRO">Home</a></li>
3773                <li class="nav-item active">
3774                  <a href="/fro/about" class="nav-link" aria-label="" target="_self">About</a></li>
3775                <li class="nav-item">
3776                  <a href="/fro/team" class="nav-link" aria-label="" target="_self">Team</a></li>
3777                <li class="nav-item">
3778                  <a href="/fro/roadmap" class="nav-link" aria-label="" target="_self">Roadmap</a></li>
3779                <li class="nav-item">
3780                  <a href="/fro/contact" class="nav-link" aria-label="" target="_self">Contact</a></li>
3781                </ul>
3782              </li>
3783            </ul>
3784          </menu></nav>
3785      <nav class="sub-navbar">
3786        <div class="navbar-container container">
3787          <a class="nav-logo" href="/fro"><svg width="70" height="20" viewBox="-60 0 385 169" fill="transparent" xmlns="http://www.w3.org/2000/svg" stroke="#386EE0" stroke-width="10"><path d="M6.5 5.00001V163.454H5L5.5 87M5.5 87V5.00001L121.5 5M5.5 87L106.5 87M121.5 5V87M121.5 5L170.5 4.99988C213.864 4.99988 232.527 13.4976 232.527 45.9891C232.527 66.3579 224.406 77.297 209.027 82.6298M121.5 166V87M121.5 87L170.5 86.9782C186.2 87.1741 199.12 86.0654 209.027 82.6298M235.027 166L209.027 82.6298" stroke-linejoin="round"></path>
3787<path d="M308 6C347.14 6 379.5 40.3357 379.5 83.5C379.5 126.664 347.14 161 308 161C268.86 161 236.5 126.664 236.5 83.5C236.5 40.3357 268.86 6 308 6Z"></path></svg></a><ul class="nav-list">
3788            <li class="nav-item">
3789              <a href="/fro" class="nav-link" aria-label="" target="_self">Home</a></li>
3790            <li class="nav-item active">
3791              <a href="/fro/about" class="nav-link" aria-label="" target="_self">About</a></li>
3792            <li class="nav-item">
3793              <a href="/fro/team" class="nav-link" aria-label="" target="_self">Team</a></li>
3794            <li class="nav-item">
3795              <a href="/fro/roadmap" class="nav-link" aria-label="" target="_self">Roadmap</a></li>
3796            <li class="nav-item">
3797              <a href="/fro/contact" class="nav-link" aria-label="" target="_self">Contact</a></li>
3798            </ul>
3799          </div>
3800        </nav>
3801      </header>
3802    <main class="container fro"><div class="post-center post-page">
3803        <article class="post-container"><div class="post-content">
3804            <h1 class="page-title">
3805              About</h1>
3806            <section>
3807              <h2 id="the-lean-fro">
3808                The Lean FRO<span class="permalink-widget inline"><a href="fro/about/#the-lean-fro" title="Permalink">🔗</a></span></h2>
3809              <p>
3810                <strong>The Lean Focused Research Organization works to make formal verification more accessible across mathematics research, software and hardware verification, and AI-assisted theorem proving.</strong> Since its formation in July 2023 as a non-profit organization under Convergent Research, the FRO pursues a focused mission to improve Lean's critical systems through enhanced scalability, usability, documentation, and proof automation while guiding Lean toward long-term self-sustainability.</p>
3811              <p>
3812                The Lean FRO is led by Chief Architect and co-founder <a href="https://leodemoura.github.io/blog/">Leonardo de Moura</a>, currently a senior principal applied scientist in the Automated Reasoning Group at Amazon Web Services. De Moura created Lean in 2013 and previously worked on automated reasoning and theorem proving at Microsoft Research and SRI International.</p>
3813              <p>
3814                Working alongside de Moura is Head of Engineering and co-founder Sebastian Ullrich and a <a href="/fro/team">team of skilled researchers and engineers</a> with specialized expertise across diverse aspects of Lean development. The Lean FRO team is globally diverse and many team members are recruited directly from the very active Lean community. The team actively engages with the community to promote Lean adoption across academic and industry contexts.</p>
3815              <p>
3816                The Lean FRO gratefully acknowledges support from its funders and supporters, including Alex Gerko, Alfred P. Sloan Foundation, Richard Merkin Foundation, Simons Foundation International, and Convergent Research.</p>
3817              </section>
3818            <section>
3819              <h2 id="a-brief-history-of-lean">
3820                A Brief History of Lean<span class="permalink-widget inline"><a href="fro/about/#a-brief-history-of-lean" title="Permalink">🔗</a></span></h2>
3821              <ul>
3822                <li>
3823                  <p>
3824                    <strong>September 2026</strong> - Anthropic <a href="https://www.anthropic.com/research/formalizing-fermats-last-theorem">announces</a> Lean formalization of Fermat's Last Theorem;
3825OpenAI's <a href="https://openai.com/index/gpt-6-astra/">GPT-6 Astra</a> helped establish a stronger prime gap bound of 186, with <a href="https://github.com/openai/PrimeGaps186">Lean formalization</a></p>
3826                  </li>
3827                <li>
3828                  <p>
3829                    <strong>August 2026</strong> - OpenAI provides <a href="https://github.com/openai/ten-proofs">Lean certificates</a> and <a href="https://openai.com/index/ten-advances-in-mathematics/">announces progress</a> on 10 research-level mathematical problems; Anthropic <a href="https://www.anthropic.com/research/riemann-zeta">announces new results</a> related to the Riemann zeta function and provides <a href="https://github.com/anthropics/zeta-23-lean">Lean formalizations</a>
3829 that pass Comparator validation; Lean FRO publishes <a href="https://lean-lang.org/fro/roadmap/y4-1/">Year 4 Part 1 Roadmap</a>; <a href="https://www.ibtimes.com/chris-hsu-how-one-programming-language-rewrote-mathematics-why-software-next-3806974">International Business Times</a> interviews Chris Hsu: 'How One Programming Language Rewrote Mathematics and Why Software Is Next'; Kim Morrison launches <a href="https://palomar-registry.org/">Palomar</a>, a Registry of Lean-Verified Mathematics</p>
3830                  </li>
3831                <li>
3832                  <p>
3833                    <strong>July 2026</strong> - Amazon Automated reasoning <a href="https://www.amazon.science/news/amazon-is-investing-in-the-lean-focused-research-organization">announces the single largest donation</a> to Lean FRO in the FRO's history; <a href="https://www.microsoft.com/en-us/research/blog/verifying-rust-cryptography-in-symcrypt-from-standards-to-code/">Microsoft Research</a> reports on how Lean, via the Aeneas toolchain, formally verifies production cryptographic algorithms in SymCrypt; <a href="https://www.newscientist.com/article/2533518-mathematicians-put-ai-to-work-on-fermats-last-theorem/">New Scientist</a> reports on AI use supporting the Lean formalization of Fermat's Last Theorem; <a href="https://kim-em.github.io/hex-dev/">the Hex project</a>, a library for computational algebra, is released; a <a href="https://lean-lang.org/eval/problems/erdos_unit_distance_conjecture_false/">1.2M line human-in-the-loop proof</a> of the falsity of the Erdos unit-distance problem is submitted to Lean Eval; <a href="https://taucetiproject.github.io/TauCeti/">Tau Ceti</a> launched, AI-authored Lean mathematics downstream of Mathlib, with human-owned roadmaps and AI adversarial review against open rubrics; <a href="https://github.com/BobDyLean/dylean">Bob DyLean</a>, a framework for the symbolic analysis of cryptographic protocols, is open-sourced; Google DeepMind <a href="https://deepmind.google/public-policy/conjecture-machines-ai-agents-and-the-new-validation-bottleneck-in-science/">publishes on AI conjecture machines</a> and Lean as the validation layer for AI-generated science</p>
3834                  </li>
3835                <li>
3836                  <p>
3837                    <strong>June 2026</strong> - Quanta Books publishes <a href="https://www.quantabooks.org/books/the-proof-in-the-code/">The Proof in the Code</a>, "the definitive account of the birth and rise of Lean"; Lean is featured as part of Simons Foundation <a href="https://www.simonsfoundation.org/2026/06/23/from-trust-to-verification-leans-impact-on-mathematics/">2025 Annual Report</a>; <a href="https://fortune.com/2026/06/01/axiom-math-econlib-antitrust-economic-theory-verified/">Fortune magazine</a> announces Axiom's EconLib, formalizing economic theory in Lean; <a href="https://comparator.live.lean-lang.org">Comparator</a>, a sandboxed judge for Lean proofs that exports and re-checks independently, is launched; <a href="https://lean-lang.org/eval/">Lean Eval</a>, a public submission-based leaderboard of hard formalization problems, is launched; <a href='https://stat-lib.github.io/'>StatLib</a>, a library for mathematical statistics, is launched; <a href="https://pramaanalabs.ai/blog/we-raised-27m-to-build-a-compiler-for-mission-critical-ai">Pramaana Labs</a> launches out of stealth with <a href="https://techcrunch.com/2026/06/17/pramaana-labs-raises-27-million-seed-round-from-khosla-ventures-to-bring-formal-verification-to-ai/">$27M from Khosla Ventures</a> for Lean-based formal verification</p>
3838                  </li>
3839                <li>
3840                  <p>
3841                    <strong>May 2026</strong> - Google DeepMind announces <a href="https://arxiv.org/abs/2605.22763v1">AlphaProof Nexus</a> and autonomous proofs of <a href="https://github.com/google-deepmind/alphaproof-nexus-results">9 Erdős problems</a>; SAIR convenes the <a href="https://sair.foundation/events/science-ai-summit-2026">Science x AI Summit</a> in Palo Alto, foregrounding Lean and AI-assisted proof discovery; NASA holds its <a href="https://nfm2026.github.io/">Formal Methods Symposium</a> with <a href="https://nfm2026.github.io/keynote_speakers/">keynotes</a> on <a href="https://lean-lang.org">Lean</a>, <a href="https://www.cslib.io/">CSLib</a> and <a href="https://aristotle.harmonic.fun/">Aristotle</a>; <a href="https://lean-dojo.github.io/TorchLean/">TorchLean</a> is released, bridging PyTorch and Lean</p>
3842                  </li>
3843                <li>
3844                  <p>
3845                    <strong>April 2026</strong> - OpenAI <a href="https://openai.com/index/introducing-gpt-5-5/">releases ChatGPT 5.5</a>, used internally by OpenAI to discover a new Lean-verified proof relating to off-diagonal Ramsey numbers; <a href="https://www.economist.com/science-and-technology/2026/04/08/ai-models-could-offer-mathematicians-a-common-language">The Economist</a> profiles Lean-powered AI math startups; <a href="https://beneficial-ai-foundation.github.io/SVIL2026/">Software Verification in Lean</a> takes place in Paris; The <a href="https://www.beneficialaifoundation.org/signal-shot">Signal Shot</a> challenge is announced;
3845 The <a href="https://competition.sair.foundation/competitions/mathematics-distillation-challenge-equational-theories-stage2/overview">SAIR Mathematics Distillation Challenge Stage 2</a> announced; <a href="https://www.newscientist.com/article/2522687-the-secret-project-to-settle-controversial-maths-proof-with-a-computer/">New Scientist</a> reports on the LANA project; <a href="https://arena.lean-lang.org">Lean Kernel Arena</a>, a public benchmarking of independent proof checkers, goes live</p>
3846                  </li>
3847                <li>
3848                  <p>
3849                    <strong>March 2026</strong> - <a href="https://spectrum.ieee.org/scenario-modeling-and-array-design-for-non-terrestrial-networks-ntns">IEEE Spectrum</a> reports on formalization in Lean of proof of sphere packing in 24-dimensions via Math, Inc.'s Gauss; The <a href="https://zen.ac.jp/en/zmc/topics/jwz-o8xr3v6f">LANA Project</a> is announced; The <a href="https://competition.sair.foundation/competitions/mathematics-distillation-challenge-equational-theories-stage1/overview">SAIR Mathematics Distillation Challenge Stage 1</a> announced; The <a href="https://github.com/leanprover/lean4">Lean GitHub repository</a> is starred over 7,500 times; <a href=" https://mistral.ai/news/leanstral">Leanstral</a>, the first open-source code agent designed for Lean 4, released</p>
3850                  </li>
3851                <li>
3852                  <p>
3853                    <strong>February 2026</strong> - <a href="https://www.wired.com/story/a-new-ai-math-ai-startup-just-cracked-4-previously-unsolved-problems/">Wired reports</a> on how Lean enables Axiom's proof of Fel's Conjecture; <a href="https://cacm.acm.org/news/math-in-the-age-of-ai/">Communications of the ACM</a> reports on Lean's critical role in verifying AI mathematical output; <a href="https://harmonic.fun/news/lean-fro-donation/">Harmonic announces</a> inaugural donation to Lean FRO to advance formal reasoning and mathematical AI</p>
3854                  </li>
3855                <li>
3856                  <p>
3857                    <strong>January 2026</strong> - Advances in <a href="https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-problems">human-AI collaborative proof development</a> yields proofs and Lean formalizations to previously open Erdős problems, <a href="https://www.newscientist.com/article/2511954-amateur-mathematicians-solve-long-standing-maths-problems-with-ai/">New Scientist</a> highlights Lean's key role in powering Harmonic's Aristotle; AxiomProver <a href="https://github.com/AxiomMath/putnam2025">solves 8 of 12 Putnam problems</a> during the Putnam competition</p>
3858                  </li>
3859                <li>
3860                  <p>
3861                    <strong>December 2025</strong> - The Lean@Google Hackathon takes place, initiating development of the <strong>SymM</strong> framework, a lightweight monadic framework for high-performance software verification; The <a href="https://arxiv.org/abs/2512.07087">Equational Theories Project</a> is completed</p>
3862                  </li>
3863                <li>
3864                  <p>
3865                    <strong>November 2025</strong> - <a href="https://www.nature.com/articles/s41586-025-09833-y">Nature</a> publishes a paper by Google DeepMind on their silver medal performance at the 2024 IMO; Lean profiled in <a href="https://venturebeat.com/ai/lean4-how-the-theorem-prover-works-and-why-its-the-new-competitive-edge-in/">VentureBeat</a> and <a href="https://www.newscientist.com/article/2503500-the-biggest-controversy-in-maths-could-be-settled-by-a-computer/">New Scientist</a></p>
3866                  </li>
3867                <li>
3868                  <p>
3869                    <strong>October 2025</strong> - Harmonic releases <a href="https://aristotle.harmonic.fun/">Aristotle</a>, a mathematical superintelligence with Lean API; <a href="https://axiommath.ai/">Axiom</a> launches, with the goal of building a quantitative super-intelligence; <a href="https://verse-lab.github.io/papers/loom-preprint.pdf">Velvet</a> is released, a verifier for imperative programs in Lean; Erdős 707 is resolved with a <a href="https://arxiv.org/abs/2510.19804">vibe-coded Lean proof</a></p>
3870                  </li>
3871                <li>
3872                  <p>
3873                    <strong>September 2025</strong>
3873 - Official launch of the <a href="https://mathlib-initiative.org/">Mathlib Initiative</a>; The Lean <a href="https://marketplace.visualstudio.com/items?itemName=leanprover.lean4&amp;ssr=false#overview">VS Code development environment</a> is installed over 100,000 times</p>
3874                  </li>
3875                <li>
3876                  <p>
3877                    <strong>August 2025</strong> - Lean FRO begins 3rd year of operations and ships the <a href="https://lean-lang.org/doc/reference/latest/releases/v4.22.0/#release-v4___22___0"><strong>grind</strong> tactic and new compiler</a>; <a href="https://www.cslib.io/">CSLib</a> project, a foundation for Computer Science in Lean, announced; The <a href="https://florisvandoorn.com/carleson/">Carleson project</a> is completed; <a href="https://google-deepmind.github.io/formal-conjectures/">DeepMind Formal Conjectures</a> project, cataloguing formalised statements of open mathematical conjectures in Lean 4, is established</p>
3878                  </li>
3879                <li>
3880                  <p>
3881                    <strong>July 2025</strong> - <a href="https://www.renaissancephilanthropy.org/news-and-insights/lean-fro-and-mathlib-receive-10m-from-xtx-markets-founder-alex-gerko-to-further-advance-the-use-of-ai-for-mathematical-research">$10MM in new funding from Alex Gerko is announced</a>. $5MM supports a new Mathlib Initiative and $5MM is awarded to Lean FRO to support development of new Lean features; Lean is awarded the <a href="https://cadeinc.org/Skolem-Award">2025 Skolem Award</a> for 2015 CADE paper "The Lean Theorem Prover (System Description)"; Aristotle (Harmonic) <a href="https://www.harmonic.fun/news/imo-gold">wins IMO gold</a> using Lean; ByteDance's Seed Prover <a href="https://seed.bytedance.com/en/blog/bytedance-seed-prover-achieves-silver-medal-score-in-imo-2025">wins IMO silver</a> using Lean; <a href="https://lean-lang.org/use-cases/veil/">Veil</a> is presented at CAV25</p>
3882                  </li>
3883                <li>
3884                  <p>
3885                    <strong>June 2025</strong> - Lean is awarded the <a href="https://www.sigplan.org/Awards/Software/#2025_Lean_Theorem_Prover">2025 ACM SIGPLAN Programming Languages Software Award</a>; SampCert, an open-source Lean library of verified differential-privacy primitives deployed in AWS Clean Rooms <a href="https://dl.acm.org/doi/10.1145/3729294">presented at PLDI 2025</a></p>
3886                  </li>
3887                <li>
3888                  <p>
3889                    <strong>May 2025</strong> - Over <a href="https://leanprover-community.github.io/teaching/courses.html">50 university-level courses</a> have been taught using Lean</p>
3890                  </li>
3891                <li>
3892                  <p>
3893                    <strong>February 2025</strong> - The <a href="https://github.com/leanprover/lean4">Lean GitHub repository</a> is starred over 5,000 times</p>
3894                  </li>
3895                <li>
3896                  <p>
3897                    <strong>January 2025</strong> - The <a href="https://github.com/leanprover-community/mathlib4">Mathlib4 GitHub repository</a> exceeds 20,000 contributions</p>
3898                  </li>
3899                <li>
3900                  <p>
3901                    <strong>December 2024</strong> - Over 30,000 installs of the Lean <a href="https://marketplace.visualstudio.com/items?itemName=leanprover.lean4">VS Code development environment</a> occur in a single calendar year</p>
3902                  </li>
3903                <li>
3904                  <p>
3905                    <strong>November 2024</strong> - <a href="https://github.com/lean-dojo/LeanCopilot">Lean Copilot</a> is covered by Scientific American in <a href="https://www.scientificamerican.com/article/mathematicians-newest-assistants-are-artificially-intelligent/">Mathematicians' Newest Assistants Are Artificially Intelligent</a></p>
3906                  </li>
3907                <li>
3908                  <p>
3909                    <strong>September 2024</strong> - The <a href="https://teorth.github.io/equational_theories/">Equational Theories project</a> is established; <a href="https://github.com/PatrickMassot/verbose-lean4">Lean Verbose</a>, a framework of controlled natural language tactics and commands, presented at ITP 2024; The <a href="https://leanprover.zulipchat.com/">Lean Community Zulip channel</a> grows to over 10,000 members</p>
3910                  </li>
3911                <li>
3912                  <p>
3913                    <strong>July 2024</strong> - AlphaProof achieves <a href="https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/">IMO silver medal performance</a> using Lean and Mathlib. The New York Times covers it in <a href="https://www.nytimes.c
3913om/2024/07/25/science/ai-math-alphaproof-deepmind.html">Move Over, Mathematicians, Here Comes AlphaProof</a>, Nature in <a href="https://www.nature.com/articles/d41586-024-02441-2">DeepMind hits milestone in solving maths problems — AI's next grand challenge</a>, MIT Technology Review in <a href="https://www.technologyreview.com/2024/07/25/1095315/google-deepminds-ai-systems-can-now-solve-complex-math-problems/">Google DeepMind's new AI systems can now solve complex math problems</a>, and Fortune in <a href="https://fortune.com/2024/07/25/google-researchers-claim-new-breakthrough-in-getting-ai-to-solve-tough-high-school-math-problems/">Google researchers claim new breakthrough in getting AI to solve tough high school math problems</a></p>
3914                  </li>
3915                <li>
3916                  <p>
3917                    <strong>June 2024</strong> - <a href="https://harmonic.fun/">Harmonic</a> launches, the first startup based on Lean. The New York Times covers it in <a href="https://www.nytimes.com/2024/09/23/technology/ai-chatbots-chatgpt-math.html">Is Math the Path to Chatbots That Don't Make Stuff Up?</a> and Sequoia Capital in <a href="https://www.sequoiacap.com/podcast/training-data-harmonic/">Training Data: Ep14</a>; Scientific American publishes <a href="https://www.scientificamerican.com/article/ai-will-become-mathematicians-co-pilot/">AI Will Become Mathematicians' 'Co-Pilot'</a>; The <a href="https://florisvandoorn.com/carleson/">Carleson project</a> is established</p>
3918                  </li>
3919                <li>
3920                  <p>
3921                    <strong>April 2024</strong> - <a href="https://aws.amazon.com/blogs/opensource/lean-into-verified-software-development/">Lean verification of AWS Cedar policies</a> is released</p>
3922                  </li>
3923                <li>
3924                  <p>
3925                    <strong>January 2024</strong> - First public launch of <a href="https://github.com/leanprover/verso">Verso</a>, the Lean authoring tool</p>
3926                  </li>
3927                <li>
3928                  <p>
3929                    <strong>December 2023</strong> - The <a href="https://imperialcollegelondon.github.io/FLT/">Fermat's Last Theorem project</a> is established</p>
3930                  </li>
3931                <li>
3932                  <p>
3933                    <strong>November 2023</strong> - The <a href="https://teorth.github.io/pfr/">Polynomial Freiman-Ruzsa conjecture project</a> is established. Quanta Magazine covers it in <a href="https://www.quantamagazine.org/a-team-of-math-proves-a-critical-link-between-addition-and-sets-20231206/">'A-Team' of Math Proves a Critical Link Between Addition and Sets</a></p>
3934                  </li>
3935                <li>
3936                  <p>
3937                    <strong>October 2023</strong> - Quanta Magazine publishes <a href="https://www.quantamagazine.org/the-deep-link-equating-math-proofs-and-computer-programs-20231011/">The Deep Link Equating Math Proofs and Computer Programs</a></p>
3938                  </li>
3939                <li>
3940                  <p>
3941                    <strong>September 2023</strong> - Lean 4.0 is officially released</p>
3942                  </li>
3943                <li>
3944                  <p>
3945                    <strong>July 2023</strong> - <a href="https://lean-lang.org/fro/">Lean FRO</a> is founded by <a href="https://leodemoura.github.io/">Leonardo de Moura</a> and <a href="https://sebasti.a.nullri.ch/">Sebastian Ullrich</a>; The New York Times publishes <a href="https://www.nytimes.com/2023/07/02/science/ai-mathematics-machine-learning.html">A.I. Is Coming for Mathematics, Too</a>; The Lean community completes the port of <a href="https://github.com/leanprover-community/mathlib4">Mathlib</a> from Lean 3 to Lean 4; <a href="https://leandojo.org/">LeanDojo</a> is presented at NeurIPS 2023</p>
3946                  </li>
3947                <li>
3948                  <p>
3949                    <strong>February 2023</strong> - Nature publishes <a href="https://www.nature.com/articles/d41586-023-00487-2">How will AI change mathematics? Rise of chatbots highlights discussion</a></p>
3950                  </li>
3951                <li>
3952                  <p>
3953                    <strong>August 2022</strong> - The <a href="https://github.com/AeneasVerif/aeneas">Aeneas verification toolchain</a> is presented at ICFP 2022; Development begins on <a href="https://github.com/leanprover-community/iris-lean">Iris-Lean</a>, a higher-order concurrent separation logic framework</p>
3954                  </li>
3955                <li>
3956                  <p>
3957                    <strong>November 2021</strong> - The Lean Community Zulip channel grows to over 5,000 members</p>
3958                  </li>
3959                <li>
3960                  <p>
3961                    <strong>September 2021</strong> - The Lean GitHub repository is starred over 1,000 times</p>
3962                  </li>
3963                <li>
3964                  <p>
3965                    <strong>August 2021</strong> - The Mathlib3 GitHub repository exceeds 10,000 contributions</p>
3966                  </li>
3967                <li>
3968                  <p>
3969                    <strong>July 2021</strong> - The <a href="https://github.com/leanprover-community/lean-liquid">Liquid Tensor Experiment project</a> is completed. Nature covers it in <a href="https://www.nature.com/articles/d41586-021-01627-2">Mathematicians welcome computer-assisted proof in 'grand unification' theory</a> and Quanta Magazine in <a href="https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/">Proof Assistant Makes Jump to Big-League Math</a></p>
3970                  </li>
3971                <li>
3972                  <p>
3973                    <strong>May 2021</strong> - The Mathlib4 GitHub repository is created</p>
3974                  </li>
3975                <li>
3976                  <p>
3977                    <strong>December 2020</strong> - The Liquid Tensor Experiment project is established</p>
3978                  </li>
3979                <li>
3980                  <p>
3981                    <strong>October 2020</strong> - Quanta Magazine publishes <a href="https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/">Building the Mathematical Library of the Future</a></p>
3982                  </li>
3983                <li>
3984                  <p>
3985                    <strong>October 2019</strong> - The <a href="https://adam.math.hhu.de/#/g/leanprover-community/nng4">Natural Number Game</a> v1.0 is released</p>
3986                  </li>
3987                <li>
3988                  <p>
3989                    <strong>January 2019</strong> - The first <a href="https://lean-forward.github.io/lean-together/2019/">Lean Together workshop</a> is hosted at Vrije Universiteit Amsterdam</p>
3990                  </li>
3991                <li>
3992                  <p>
3993                    <strong>April 2018</strong> - Lean 4 development begins</p>
3994                  </li>
3995                <li>
3996                  <p>
3997                    <strong>February 2018</strong> - The Lean Community Zulip channel is established</p>
3998                  </li>
3999                <li>
4000                  <p>
4001                    <strong>July 2017</strong> - The Mathlib3 mathematical library is created</p>
4002                  </li>
4003                <li>
4004                  <p>
4005                    <strong>June 2017</strong>
4005 - The <a href="https://www.newton.ac.uk/event/bpr/">Big Proof Programme</a>, focused on bringing proof technology into mainstream mathematical practice, takes place at Isaac Newton Institute for Mathematical Sciences</p>
4006                  </li>
4007                <li>
4008                  <p>
4009                    <strong>January 2017</strong> - Lean 3.0 is officially released</p>
4010                  </li>
4011                <li>
4012                  <p>
4013                    <strong>August 2015</strong> - "The Lean Theorem Prover (System Description)" is published at CADE-25</p>
4014                  </li>
4015                <li>
4016                  <p>
4017                    <strong>January 2015</strong> - The first university course using Lean, <a href="https://leanprover.github.io/cmu-15815-s15/index.html">15–815 Interactive Theorem Proving</a>, is taught at Carnegie Mellon University</p>
4018                  </li>
4019                <li>
4020                  <p>
4021                    <strong>June 2014</strong> - Official release of Lean 0.1</p>
4022                  </li>
4023                <li>
4024                  <p>
4025                    <strong>July 2013</strong> - First commit to the Lean repository
4026</p>
4027                  </li>
4028                </ul>
4029              </section>
4030            </div>
4031          </article></div>
4032      </main><footer role="contentinfo" aria-label="Site footer"><div class="footer-grid container">
4033        <nav class="footer-column" aria-label="LEAN">
4034          <a href="/"><svg width="80" height="40" viewBox="0 0 486 169" xmlns="http://www.w3.org/2000/svg" stroke="white" fill="transparent" stroke-width="10"><path d="M206.333 5.67949H105.667M206.333 5.67949L243.25 84.5M206.333 5.67949V84.5M243.25 84.5H317.549M243.25 84.5L279.667 163.321L280.889 163.318L317.549 84.5M206.333 84.5V163.321H5V5M206.333 84.5H105.667M317.549 84.5L353 5.67949M353 5.67949V164M353 5.67949H353.667L480.333 163.454H481V5" stroke-linecap="round" stroke-linejoin="round"></path></svg></a></nav>
4035        <nav class="footer-column" aria-label="LEAN">
4036          <h3 id="get-started" class="footer-heading">
4037            Get Started</h3>
4038          <ul class="footer-links">
4039            <li>
4040              <a href="/install" class="footer-text" target="_self">Install</a></li>
4041            <li>
4042              <a href="/learn" class="footer-text" target="_self">Learn</a></li>
4043            <li>
4044              <a href="/community" class="footer-text" target="_self">Community</a></li>
4045            <li>
4046              <a href="https://live.lean-lang.org/?from=lean" class="footer-text" target="_blank">Playground</a></li>
4047            <li>
4048              <a href="https://reservoir.lean-lang.org/" class="footer-text" target="_blank">Reservoir</a></li>
4049            </ul>
4050          </nav>
4051        <nav class="footer-column" aria-label="Documentation">
4052          <h3 id="documentation" class="footer-heading">
4053            Documentation</h3>
4054          <ul class="footer-links">
4055            <li>
4056              <a href="/doc/reference/latest/" class="footer-text" target="_self">Language reference</a></li>
4057            <li>
4058              <a href="/doc/api/" class="footer-text" target="_self">Lean API</a></li>
4059            <li>
4060              <a href="/use-cases" class="footer-text" target="_self">Use cases</a></li>
4061            <li>
4062              <a href="/faq" class="footer-text" target="_self">FAQ</a></li>
4063            <li>
4064              <a href="/learn#how-to-cite-lean" class="footer-text" target="_self">Cite Lean</a></li>
4065            </ul>
4066          </nav>
4067        <nav class="footer-column" aria-label="Resources">
4068          <h3 id="resources" class="footer-heading">
4069            Resources</h3>
4070          <ul class="footer-links">
4071            <li>
4072              <a href="https://marketplace.visualstudio.com/items?itemName=leanprover.lean4" class="footer-text" target="_blank">VS Code extension</a></li>
4073            <li>
4074              <a href="https://loogle.lean-lang.org/" class="footer-text" target="_blank">Loogle!</a></li>
4075            <li>
4076              <a href="https://verso.lean-lang.org/" class="footer-text" target="_blank">Verso</a></li>
4077            <li>
4078              <a href="https://leanprover-community.github.io/" class="footer-text" target="_blank">Mathlib</a></li>
4079            <li>
4080              <a href="https://www.cslib.io/" class="footer-text" target="_blank">CSLib</a></li>
4081            </ul>
4082          </nav>
4083        <nav class="footer-column" aria-label="FRO">
4084          <h3 id="fro" class="footer-heading">
4085            FRO</h3>
4086          <ul class="footer-links">
4087            <li>
4088              <a href="/fro" class="footer-text" target="_self">Vision</a></li>
4089            <li>
4090              <a href="/fro/team" class="footer-text" target="_self">Team</a></li>
4091            <li>
4092              <a href="/fro/roadmap/y4-1" class="footer-text" target="_self">Roadmap</a></li>
4093            <li>
4094              <a href="https://leodemoura.github.io/blog/" class="footer-text" target="_blank">Founder's Blog</a></li>
4095            </ul>
4096          </nav>
4097        <nav class="footer-column" aria-label="Policies">
4098          <h3 id="policies" class="footer-heading">
4099            Policies</h3>
4100          <ul class="footer-links">
4101            <li>
4102              <a href="/privacy" class="footer-text" target="_self">Privacy Policy</a></li>
4103            <li>
4104              <a href="/terms" class="footer-text" target="_self">Terms of Use</a></li>
4105            <li>
4106              <a href="/trademark-policy" class="footer-text" target="_self">Lean Trademark Policy</a></li>
4107            </ul>
4108          </nav>
4109        </div>
4110      <div class="footer-divider container" role="separator"></div>
4111      <div class="footer-bottom container">
4112        <div class="footer-copy">
4113          © 2026 Lean FRO. All rights reserved.</div>
4114        <div class="footer-socials">
4115          <label class="theme-switch"><input type="checkbox" class="change-theme"><div class="switch-container">
4116              <span class="slider"></span></div>
4117            </label><a href="https://bsky.app/profile/lean-lang.org" aria-label="Bluesky"><svg width="20" height="20" viewBox="0 0 568 501" fill="none" xmlns="http://www.w3.org/2000/svg"><path d="M123.121 33.6637C188.241 82.5526 258.281 181.681 284 234.873C309.719 181.681 379.759 82.5526 444.879 33.6637C491.866 -1.61183 568 -28.9064 568 57.9464C568 75.2916 558.055 203.659 552.222 224.501C531.947 296.954 458.067 315.434 392.347 304.249C507.222 323.8 536.444 388.56 473.333 453.32C353.473 576.312 301.061 422.461 287.631 383.039C285.169 375.812 284.017 372.431 284 375.306C283.983 372.431 282.831 375.812 280.369 383.039C266.939 422.461 214.527 576.312 94.6667 453.32C31.5556 388.56 60.7778 323.8 175.653 304.249C109.933 315.434 36.0535 296.954 15.7778 224.501C9.94525 203.659 0 75.2916 0 57.9464C0 -28.9064 76.1345 -1.61183 123.121 33.6637Z" fill="white"></path></svg></a><a href="https://www.linkedin.com/company/lean-fro" aria-label="LinkedIn"><img width="20" src="../../static/svg/linkedin-white.png" alt="LinkedIn"></a><a href="https://functional.cafe/@leanprover" aria-label="Mastodon"><svg width="20" height="20" viewBox="0 0 74 79" fill="white" xmlns="http://www.w3.org/2000/svg"><path d="M73.7014 17.9592C72.5616 9.62034 65.1774 3.04876 56.424 1.77536C54.9472 1.56019 49.3517 0.7771 36.3901 0.7771H36.2933C23.3281 0.7771 20.5465 1.56019 19.0697 1.77536C10.56 3.01348 2.78877 8.91838 0.903306 17.356C-0.00357857 21.5113 -0.100361 26.1181 0.068112 30.3439C0.308275 36.404 0.354874 42.4535 0.91406 48.489C1.30064 52.498 1.97502 56.4751 2.93215 60.3905C4.72441 67.6217 11.9795 73.6395 19.0876 76.0945C26.6979 78.6548 34.8821 79.0799 42.724 77.3221C43.5866 77.1245 44.4398 76.8953 45.2833 76.6342C47.1867 76.0381 49.4199 75.3714 51.0616 74.2003C51.0841 74.1839 51.1026 74.1627 51.1156 74.1382C51.1286 74.1138 51.1359 74.0868 51.1368 74.0592V68.2108C51.1364 68.185 51.1302 68.1596 51.1185 68.1365C51.1069 68.1134 51.0902 68.0932 51.0695 68.0773C51.0489 68.0614 51.0249 68.0503 50.9994 68.0447C50.9738 68.0391 50.9473 68.0392 50.9218 68.045C45.8976 69.226 40.7491 69.818 35.5836 69.8087C26.694 69.8087 24.3031 65.6569 23.6184 63.9285C23.0681 62.4347 22.7186 60.8764 22.5789 59.2934C22.5775 59.2669 22.5825 59.2403 22.5934 59.216C22.6043 59.1916 22.621 59.1702 22.6419 59.1533C22.6629 59.1365 22.6876 59.1248 22.714 59.1191C22.7404 59.1134 22.7678 59.1139 22.794 59.1206C27.7345 60.2936 32.799 60.8856 37.8813 60.8843C39.1036 60.8843 40.3223 60.8843 41.5447 60.8526C46.6562 60.7115 52.0437 60.454 57.0728 59.4874C57.1983 59.4628 57.3237 59.4416 57.4313 59.4098C65.3638 57.9107 72.9128 53.2051 73.6799 41.2895C73.7086 40.8204 73.7803 36.3758 73.7803 35.889C73.7839 34.2347 74.3216 24.1533 73.7014 17.9592ZM61.4925 47.6918H53.1514V27.5855C53.1514 23.3526 51.3591 21.1938 47.7136 21.1938C43.7061 21.1938 41.6988 23.7476 41.6988 28.7919V39.7974H33.4078V28.7919C33.4078 23.7476 31.3969 21.1938 27.3894 21.1938C23.7654 21.1938 21.9552 23.3526 21.9516 27.5855V47.6918H13.6176V26.9752C13.6176 22.7423 14.7157 19.3795 16.9118 16.8868C19.1772 14.4 22.1488 13.1231 25.8373 13.1231C30.1064 13.1231 33.3325 14.7386 35.4832 17.9662L37.5587 21.3949L39.6377 17.9662C41.7884 14.7386 45.0145 13.1231 49.2765 13.1231C52.9614 13.1231 55.9329 14.4 58.2055 16.8868C60.4017 19.3772 61.4997 22.74 61.4997 26.9752L61.4925 47.6918Z" fill="inherit"></path></svg></a><a href="https://x.com/leanprover" aria-label="X (Twitter)"><svg width="20" height="20" viewBox="0 0 1200 1227" fill="none" xmlns="http://www.w3.org/2000/svg"><path d="M714.163 519.284L1160.89 0H1055.03L667.137 450.887L357.328 0H0L468.492 681.821L0 1226.37H105.866L515.491 750.218L842.672 1226.37H1200L714.137 519.284H714.163ZM569.165 687.828L521.697 619.934L144.011 79.6944H306.615L611.412 515.685L658.88 583.579L1055.08 1150.3H892.476L569.165 687.854V687.828Z" fill="white"></path></svg></a><a href="https://leanprover.zulipchat.com/" aria-label="Zulip"><svg width="20" height="20" viewBox="0 0 25 25" fill="none" xmlns="http://www.w3.org/2000/svg"><path d="M25 3.72273C25 4.98879 24.3687 6.10367 23.4007 6.78394L14.0783 14.2669C13.9099 14.3992 13.6785 14.1913 13.8047 14.0023L17.2348 7.86103C17.3401 7.69096 17.2138 7.4831 17.0034 7.4831H3.74579C1.6835 7.4831 0 5.80133 0 3.74163C0 1.68193 1.6835 0.000157697 3.74579 0.000157697H21.2542C23.3165 -0.0187386 25 1.66303 25 3.72273ZM3.74579 25H21.2542C23.3165 25 25 23.3182 25 21.2585C25 19.1988 23.3165 17.5171 21.2542 17.5171H7.99663C7.80724 17.5171 7.68098 17.3092 7.76515 17.1391L11.1953 10.9978C11.3215 10.8278 11.0901 10.601 10.9217 10.7333L1.59933 18.2162C0.631313 18.8776 0 19.9925 0 21.2585C0 23.3182 1.6835 25 3.74579 25Z" fill="white"></path></svg></a><a href="https://github.com/leanprover/" aria-label="GitHub"><img width="20" src="../../static/svg/github-white.svg" alt="GitHub"></a></div>
4118        </div>
4119      </footer>
4119<script src="-verso-data/theme.js"></script>
4119
4120    
4120<script src="-verso-data/copy.js"></script>
4120
4121    
4121<script src="-verso-data/motion.js"></script>
4121
4122    
4122<script src="-verso-data/navbar.js"></script>
4122
4123    
4123<script id="MathJax-script" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
4123
4124    </body>
4125  </html>
4126

Line numbers count LF bytes from the start of the resource, as the search results do. Vendor segments are library code the classifier recognised; they are stored but not indexed. Bytes are shown as Latin1 characters, one per byte.