-
Notifications
You must be signed in to change notification settings - Fork 0
/
lean.bib
1567 lines (1487 loc) · 71.8 KB
/
lean.bib
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
# To normalize:
# bibtool --preserve.key.case=on --preserve.keys=on --pass.comments=on --print.use.tab=off -s -i lean.bib -o lean.bib
@InProceedings{ AGLST23,
author = {Avigad, Jeremy and Goldberg, Lior and Levit, David and
Seginer, Yoav and Titelman, Alon},
title = {{A Proof-Producing Compiler for Blockchain Applications}},
booktitle = {14th International Conference on Interactive Theorem
Proving (ITP 2023)},
pages = {7:1--7:19},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-284-6},
issn = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/opus/volltexte/2023/18382},
urn = {urn:nbn:de:0030-drops-183820},
doi = {10.4230/LIPIcs.ITP.2023.7},
annote = {Keywords: formal verification, smart contracts,
interactive proof systems},
tags = {formalization, lean3}
}
@InProceedings{ AngdinataXu23,
author = {Angdinata, David Kurniadi and Xu, Junyan},
title = {{An Elementary Formal Proof of the Group Law on
Weierstrass Elliptic Curves in Any Characteristic}},
booktitle = {14th International Conference on Interactive Theorem
Proving (ITP 2023)},
pages = {6:1--6:19},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-284-6},
issn = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/opus/volltexte/2023/18381},
urn = {urn:nbn:de:0030-drops-183817},
doi = {10.4230/LIPIcs.ITP.2023.6},
annote = {Keywords: formal math, algebraic geometry, elliptic curve,
group law, Lean, mathlib},
tags = {formalization, lean3}
}
@Book{ Avig14,
author = "Avigad, Jeremy and {de Moura}, Leonardo and Kong, Soonho",
title = {{Theorem Proving in Lean}},
year = "2014",
link = "\url{https://leanprover.github.io/tutorial/tutorial.pdf}",
publisher = "Carnegie Mellon University"
}
@Book{ Avig17,
author = "Avigad, Jeremy and Lewis, Robert Y. and {van Doorn},
Floris",
title = {{Logic and Proof}},
year = "2017",
link = "\url{https://avigad.github.io/logic_and_proof}",
publisher = "Carnegie Mellon University"
}
@InProceedings{ AvigadCarneiroHudon19,
author = {Jeremy Avigad and Mario M. Carneiro and Simon Hudon},
title = {Data Types as Quotients of Polynomial Functors},
booktitle = {10th International Conference on Interactive Theorem
Proving, {ITP} 2019, September 9-12, 2019, Portland, OR,
{USA}},
pages = {6:1--6:19},
year = {2019},
url = {https://doi.org/10.4230/LIPIcs.ITP.2019.6},
doi = {10.4230/LIPIcs.ITP.2019.6},
timestamp = {Fri, 27 Sep 2019 15:57:06 +0200},
biburl = {https://dblp.org/rec/conf/itp/AvigadCH19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
website = {https://github.com/avigad/qpf}
}
@InProceedings{ Baanen20,
author = {Anne Baanen},
editor = {Nicolas Peltier and Viorica Sofronie{-}Stokkermans},
title = {A Lean Tactic for Normalising Ring Expressions with
Exponents (Short Paper)},
booktitle = {Automated Reasoning - 10th International Joint Conference,
{IJCAR} 2020, Paris, France, July 1-4, 2020, Proceedings,
Part {II}},
series = {Lecture Notes in Computer Science},
volume = {12167},
pages = {21--27},
publisher = {Springer},
year = {2020},
url = {https://doi.org/10.1007/978-3-030-51054-1\_2},
doi = {10.1007/978-3-030-51054-1\_2},
timestamp = {Thu, 06 Aug 2020 21:49:45 +0200},
biburl = {https://dblp.org/rec/conf/cade/Baanen20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
tags = {about-mathlib, lean3}
}
@InProceedings{ Baanen22,
author = {Baanen, Anne},
title = {{Use and Abuse of Instance Parameters in the Lean
Mathematical Library}},
booktitle = {13th International Conference on Interactive Theorem
Proving (ITP 2022)},
pages = {4:1--4:20},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-252-5},
issn = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/opus/volltexte/2022/16713},
urn = {urn:nbn:de:0030-drops-167131},
doi = {10.4230/LIPIcs.ITP.2022.4},
annote = {Keywords: formalization of mathematics, dependent type
theory, typeclasses, algebraic hierarchy, Lean prover},
tags = {about-mathlib, lean3}
}
@InProceedings{ BaanenBCD23,
author = {Anne Baanen and Alex J. Best and Nirvana Coppola and
Sander R. Dahmen},
editor = {Robbert Krebbers and Dmitriy Traytel and Brigitte Pientka
and Steve Zdancewic},
title = {Formalized Class Group Computations and Integral Points on
Mordell Elliptic Curves},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International
Conference on Certified Programs and Proofs, {CPP} 2023,
Boston, MA, USA, January 16-17, 2023},
pages = {47--62},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575682},
doi = {10.1145/3573105.3575682},
tags = {formalization, lean3},
timestamp = {Fri, 13 Jan 2023 13:05:42 +0100},
biburl = {https://dblp.org/rec/conf/cpp/BaanenBCD23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@InProceedings{ BaanenDahmenNarayananNuccio21,
author = {Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni
and N{uccio Mortarino Majno di Capriglio}, Filippo A. E.},
title = {A Formalization of {D}edekind {D}omains an {C}lass
{G}roups of {G}lobal {F}ields},
booktitle = {12th International Conference on Interactive Theorem
Proving (ITP 2021)},
pages = {5:1--5:19},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-188-7},
issn = {1868-8969},
year = {2021},
volume = {193},
editor = {Cohen, Liron and Kaliszyk, Cezary},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.5},
urn = {urn:nbn:de:0030-drops-139004},
doi = {10.4230/LIPIcs.ITP.2021.5},
annote = {Keywords: formal math, algebraic number theory,
commutative algebra, Lean, mathlib},
tags = {formalization, lean3}
}
@Article{ BaanenDahmenNarayananNuccio22,
author = {Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni
and N{uccio Mortarino Majno di Capriglio}, Filippo A. E.},
title = {A formalization of {D}edekind domains and class groups of
global fields},
journal = {J. Automat. Reason.},
fjournal = {Journal of Automated Reasoning},
volume = {66},
year = {2022},
number = {4},
pages = {611--637},
issn = {0168-7433,1573-0670},
mrclass = {03B35 (11R29 13C20)},
mrnumber = {4505023},
doi = {10.1007/s10817-022-09644-0},
url = {https://doi.org/10.1007/s10817-022-09644-0},
tags = {formalization, lean3}
}
@Booklet{ Best2021,
author = {Alexander Best},
title = {Automatically Generalizing Theorems Using Typeclasses},
howpublished = {EasyChair Preprint no. 6216},
url = {https://easychair.org/publications/preprint/KLfT},
year = {2021},
tags = {about-mathlib, lean3}
}
@InProceedings{ BestBirkbeckBrascaRodriguez23,
author = {Best, Alex J. and Birkbeck, Christopher and Brasca,
Riccardo and Rodriguez Boidi, Eric},
title = {{Fermat’s Last Theorem for Regular Primes}},
booktitle = {14th International Conference on Interactive Theorem
Proving (ITP 2023)},
pages = {36:1--36:8},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-284-6},
issn = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/opus/volltexte/2023/18411},
urn = {urn:nbn:de:0030-drops-184115},
doi = {10.4230/LIPIcs.ITP.2023.36},
annote = {Keywords: Fermat’s Last Theorem, Cyclotomic fields,
Interactive theorem proving, Lean},
tags = {formalization, lean3}
}
@Article{ BordgCavalleri2021,
author = {Anthony Bordg and Nicol{\`{o}} Cavalleri},
title = {Elements of Differential Geometry in Lean: {A} Report for
Mathematicians},
journal = {CoRR},
volume = {abs/2108.00484},
year = {2021},
url = {https://arxiv.org/abs/2108.00484},
eprinttype = {arXiv},
eprint = {2108.00484},
timestamp = {Thu, 05 Aug 2021 14:27:08 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2108-00484.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
tags = {formalization, lean3}
}
@Article{ BrowningLutz22,
author = {Thomas Browning and Patrick Lutz},
title = {Formalizing Galois Theory},
journal = {Experimental Mathematics},
volume = {31},
number = {2},
pages = {413-424},
year = {2022},
publisher = {Taylor & Francis},
doi = {10.1080/10586458.2021.1986176},
url = {https://doi.org/10.1080/10586458.2021.1986176},
eprint = {https://doi.org/10.1080/10586458.2021.1986176},
tags = {formalization, lean3}
}
@InProceedings{ Buch18,
author = {Ulrik Buchholtz and Floris {van Doorn} and Egbert Rijke},
title = {Higher Groups in Homotopy Type Theory},
booktitle = {Proceedings of the 33rd Annual {ACM/IEEE} Symposium on
Logic in Computer Science, {LICS} 2018, Oxford, UK, July
09-12, 2018},
pages = {205--214},
year = {2018},
crossref = {DBLP:conf/lics/2018},
url = {https://doi.org/10.1145/3209108.3209150},
doi = {10.1145/3209108.3209150}
}
@InProceedings{ BuzzardCommelinMassot20,
author = {Kevin Buzzard and Johan Commelin and Patrick Massot},
title = {Formalising perfectoid spaces},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International
Conference on Certified Programs and Proofs, {CPP} 2020,
New Orleans, LA, USA, January 20-21, 2020},
pages = {299--312},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373830},
doi = {10.1145/3372885.3373830},
timestamp = {Thu, 23 Jan 2020 16:12:31 +0100},
biburl = {https://dblp.org/rec/conf/cpp/BuzzardCM20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
website = {https://leanprover-community.github.io/lean-perfectoid-spaces/},
tags = {formalization, lean3}
}
@Misc{ BuzzardHLLFM21,
title = {Schemes in Lean},
author = {Kevin Buzzard and Chris Hughes and Kenny Lau and Amelia
Livingston and Ramon Fernández Mir and Scott Morrison},
year = {2021},
eprint = {2101.02602},
archiveprefix = {arXiv},
primaryclass = {math.AG},
url = {https://arxiv.org/abs/2101.02602},
tags = {formalization, lean3}
}
@InProceedings{ Carneiro19,
author = {Mario M. Carneiro},
title = {Formalizing Computability Theory via Partial Recursive
Functions},
booktitle = {10th International Conference on Interactive Theorem
Proving, {ITP} 2019, September 9-12, 2019, Portland, OR,
{USA}},
pages = {12:1--12:17},
year = {2019},
url = {https://doi.org/10.4230/LIPIcs.ITP.2019.12},
doi = {10.4230/LIPIcs.ITP.2019.12},
timestamp = {Fri, 27 Sep 2019 15:57:06 +0200},
biburl = {https://dblp.org/rec/conf/itp/Carneiro19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
website = {https://github.com/leanprover-community/mathlib/tree/master/src/computability},
tags = {formalization, lean3}
}
@Misc{ CarneiroMaster,
author = {Mario Carneiro},
title = {The Type Theory of Lean},
eprint = {https://github.com/digama0/lean-type-theory/releases},
note = {Master thesis},
year = {2019},
abstract = {Meta-theoretic properties of Lean 3, including
soundness.},
tags = {about-lean, lean3}
}
@InProceedings{ Clune23,
author = {Joshua Clune},
editor = {Robbert Krebbers and Dmitriy Traytel and Brigitte Pientka
and Steve Zdancewic},
title = {A Formalized Reduction of Keller's Conjecture},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International
Conference on Certified Programs and Proofs, {CPP} 2023,
Boston, MA, USA, January 16-17, 2023},
pages = {90--101},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575669},
doi = {10.1145/3573105.3575669},
tags = {formalization, lean3},
timestamp = {Fri, 13 Jan 2023 13:05:42 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Clune23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@InProceedings{ CommelinLewis21,
author = {Commelin, Johan and Lewis, Robert Y.},
title = {Formalizing the Ring of Witt Vectors},
year = {2021},
isbn = {9781450382991},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3437992.3439919},
doi = {10.1145/3437992.3439919},
abstract = {The ring of Witt vectors W R over a base ring R is an
important tool in algebraic number theory and lies at the
foundations of modern p-adic Hodge theory. W R has the
interesting property that it constructs a ring of
characteristic 0 out of a ring of characteristic p > 1,
and it can be used more specifically to construct from a
finite field containing ℤ/pℤ the corresponding
unramified field extension of the p-adic numbers ℚp
(which is unique up to isomorphism). We formalize the
notion of a Witt vector in the Lean proof assistant, along
with the corresponding ring operations and other algebraic
structure. We prove in Lean that, for prime p, the ring of
Witt vectors over ℤ/pℤ is isomorphic to the ring of
p-adic integers ℤp. In the process we develop idioms to
cleanly handle calculations of identities between
operations on the ring of Witt vectors. These calculations
are intractable with a naive approach, and require a proof
technique that is usually skimmed over in the informal
literature. Our proofs resemble the informal arguments
while being fully rigorous.},
booktitle = {Proceedings of the 10th ACM SIGPLAN International
Conference on Certified Programs and Proofs},
pages = {264–277},
numpages = {14},
keywords = {ring theory, formal math, proof assistant, Lean, number
theory},
location = {Virtual, Denmark},
series = {CPP 2021},
website = {https://leanprover-community.github.io/witt-vectors/},
tags = {formalization, lean3}
}
@InProceedings{ DahmenHolzlLewis19,
author = {Sander R. Dahmen and Johannes H{\"{o}}lzl and Robert Y.
Lewis},
title = {Formalizing the Solution to the Cap Set Problem},
booktitle = {10th International Conference on Interactive Theorem
Proving, {ITP} 2019, September 9-12, 2019, Portland, OR,
{USA}},
pages = {15:1--15:19},
year = {2019},
url = {https://doi.org/10.4230/LIPIcs.ITP.2019.15},
doi = {10.4230/LIPIcs.ITP.2019.15},
timestamp = {Mon, 23 Sep 2019 17:27:15 +0200},
biburl = {https://dblp.org/rec/conf/itp/DahmenHL19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
website = {https://github.com/lean-forward/cap_set_problem},
tags = {formalization, lean3}
}
@InProceedings{ deFrutos22,
author = {de Frutos-Fern\'{a}ndez, Mar{\'\i}a In\'{e}s},
title = {{Formalizing the Ring of Ad\`{e}les of a Global Field}},
booktitle = {13th International Conference on Interactive Theorem
Proving (ITP 2022)},
pages = {14:1--14:18},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-252-5},
issn = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/opus/volltexte/2022/16723},
urn = {urn:nbn:de:0030-drops-167232},
doi = {10.4230/LIPIcs.ITP.2022.14},
annote = {Keywords: formal math, algebraic number theory, class
field theory, Lean, mathlib},
tags = {formalization, lean3}
}
@InProceedings{ deFrutos23,
author = {de Frutos-Fern\'{a}ndez, Mar{\'\i}a In\'{e}s},
title = {{Formalizing Norm Extensions and Applications to Number
Theory}},
booktitle = {14th International Conference on Interactive Theorem
Proving (ITP 2023)},
pages = {13:1--13:18},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-284-6},
issn = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/opus/volltexte/2023/18388},
urn = {urn:nbn:de:0030-drops-183880},
doi = {10.4230/LIPIcs.ITP.2023.13},
annote = {Keywords: formal mathematics, Lean, mathlib, algebraic
number theory, p-adic analysis, Galois representations,
p-adic Hodge theory},
tags = {formalization, lean3}
}
@InProceedings{ deFrutosNuccio24,
author = {de Frutos-Fern\'{a}ndez, Mar\'{\i}a In\'{e}s and N{uccio
Mortarino Majno di Capriglio}, Filippo A. E.},
title = {A Formalization of Complete Discrete Valuation Rings and
Local Fields},
year = {2024},
isbn = {9798400704888},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3636501.3636942},
doi = {10.1145/3636501.3636942},
abstract = {Local fields, and fields complete with respect to a
discrete valuation, are essential objects in commutative
algebra, with applications to number theory and algebraic
geometry. We formalize in Lean the basic theory of
discretely valued fields. In particular, we prove that the
unit ball with respect to a discrete valuation on a field
is a discrete valuation ring and, conversely, that the adic
valuation on the field of fractions of a discrete valuation
ring is discrete. We define finite extensions of valuations
and of discrete valuation rings, and prove some
localization results. Building on this general theory, we
formalize the abstract definition and some fundamental
properties of local fields. As an application, we show that
finite extensions of the field ℚp of p-adic numbers and
of the field Fp((X)) of Laurent series over Fp are local
fields.},
booktitle = {Proceedings of the 13th ACM SIGPLAN International
Conference on Certified Programs and Proofs {(CPP '24)}},
pages = {190–204},
numpages = {15},
keywords = {mathlib, local fields, formal mathematics, discrete
valuation rings, algebraic number theory, Lean},
series = {CPP 2024},
tags = {formalization, lean3}
}
@Misc{ DeMoura15,
author = "{de Moura}, Leonardo and Avigad, Jeremy and Kong, Soonho
and Roux, Cody",
title = {{Elaboration in Dependent Type Theory}},
link = "\url{https://arxiv.org/pdf/1505.04324.pdf}",
year = "2015",
abstract = {Elaboration in Lean 2},
tags = {about-lean, lean2}
}
@InProceedings{ DeMouraKongAvigadVanDoornvonRaumer,
author = {Leonardo Mendonça {de Moura} and Soonho Kong and Jeremy
Avigad and Floris {van Doorn} and Jakob {von Raumer}},
title = {The Lean Theorem Prover (System Description)},
booktitle = {Automated Deduction - CADE-25 - 25th International
Conference on Automated Deduction, Berlin, Germany, August
1-7, 2015, Proceedings},
pages = {378--388},
year = {2015},
crossref = {DBLP:conf/cade/2015},
url = "\url{https://doi.org/10.1007/978-3-319-21401-6_26}",
doi = {10.1007/978-3-319-21401-6\_26},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/MouraKADR15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
abstract = {System description of Lean 2},
tags = {about-lean, lean2}
}
@InProceedings{ deMouraUllrich2021,
author = "Moura, Leonardo de and Ullrich, Sebastian",
editor = "Platzer, Andr{\'e} and Sutcliffe, Geoff",
title = "The Lean 4 Theorem Prover and Programming Language",
booktitle = "Automated Deduction -- CADE 28",
year = "2021",
publisher = "Springer International Publishing",
address = "Cham",
pages = "625--635",
abstract = "Lean 4 is a reimplementation of the Lean interactive
theorem prover (ITP) in Lean itself. It addresses many
shortcomings of the previous versions and contains many new
features. Lean 4 is fully extensible: users can modify and
extend the parser, elaborator, tactics, decision
procedures, pretty printer, and code generator. The new
system has a hygienic macro system custom-built for ITPs.
It contains a new typeclass resolution procedure based on
tabled resolution, addressing significant performance
problems reported by the growing user base. Lean 4 is also
an efficient functional programming language based on a
novel programming paradigm called functional but in-place.
Efficient code generation is crucial for Lean users because
many write custom proof automation procedures in Lean
itself.",
isbn = "978-3-030-79876-5",
url = {https://link.springer.com/chapter/10.1007/978-3-030-79876-5_37},
tags = {lean4, about-lean}
}
@InProceedings{ DilliesMehta22,
author = {Dillies, Ya\"{e}l and Mehta, Bhavik},
title = {{Formalising Szemer\'{e}di’s Regularity Lemma in Lean}},
booktitle = {13th International Conference on Interactive Theorem
Proving (ITP 2022)},
pages = {9:1--9:19},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-252-5},
issn = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/opus/volltexte/2022/16718},
urn = {urn:nbn:de:0030-drops-167185},
doi = {10.4230/LIPIcs.ITP.2022.9},
annote = {Keywords: Lean, formalisation, formal proof, graph theory,
combinatorics, additive combinatorics, Szemer\'{e}di’s
Regularity Lemma, Roth’s Theorem},
tags = {formalization, lean3}
}
@InProceedings{ Door16,
author = {Floris {van Doorn}},
title = {Constructing the propositional truncation using
non-recursive HITs},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on
Certified Programs and Proofs, Saint Petersburg, FL, USA,
January 20-22, 2016},
pages = {122--129},
year = {2016},
crossref = {DBLP:conf/cpp/2016},
url = {https://doi.org/10.1145/2854065.2854076},
doi = {10.1145/2854065.2854076},
timestamp = {Tue, 06 Nov 2018 16:59:23 +0100},
biburl = {https://dblp.org/rec/bib/conf/cpp/Doorn16},
bibsource = {dblp computer science bibliography, https://dblp.org},
tags = {formalization, lean2}
}
@InProceedings{ Door17,
author = {Floris {van Doorn} and Jakob {von Raumer} and Ulrik
Buchholtz},
title = {Homotopy Type Theory in Lean},
booktitle = {Interactive Theorem Proving - 8th International
Conference, {ITP} 2017, Bras{\'{\i}}lia, Brazil, September
26-29, 2017, Proceedings},
pages = {479--495},
year = {2017},
crossref = {DBLP:conf/itp/2017},
url = "\url{https://doi.org/10.1007/978-3-319-66107-0_30}",
doi = {10.1007/978-3-319-66107-0\_30},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/bib/conf/itp/DoornRB17},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@InProceedings{ Door21,
author = {Floris {van Doorn}},
title = {{Formalized Haar Measure}},
booktitle = {12th International Conference on Interactive Theorem
Proving (ITP 2021)},
pages = {18:1--18:17},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-188-7},
issn = {1868-8969},
year = {2021},
volume = {193},
editor = {Cohen, Liron and Kaliszyk, Cezary},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/opus/volltexte/2021/13913},
urn = {urn:nbn:de:0030-drops-139139},
doi = {10.4230/LIPIcs.ITP.2021.18},
annote = {Keywords: Haar measure, measure theory, Bochner integral,
Lean, interactive theorem proving, formalized mathematics},
tags = {formalization, lean3}
}
@InProceedings{ DoornMN23,
author = {Floris van Doorn and Patrick Massot and Oliver Nash},
editor = {Robbert Krebbers and Dmitriy Traytel and Brigitte Pientka
and Steve Zdancewic},
title = {Formalising the h-Principle and Sphere Eversion},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International
Conference on Certified Programs and Proofs, {CPP} 2023,
Boston, MA, USA, January 16-17, 2023},
pages = {121--134},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575688},
doi = {10.1145/3573105.3575688},
tags = {formalization, lean3},
timestamp = {Fri, 13 Jan 2023 13:05:42 +0100},
biburl = {https://dblp.org/rec/conf/cpp/DoornMN23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@Article{ DupuisLewisMacbeth22,
author = {Dupuis, Fr\'{e}d\'{e}ric and Lewis, Robert Y. and Macbeth,
Heather},
title = {{Formalized functional analysis with semilinear maps}},
booktitle = {13th International Conference on Interactive Theorem
Proving (ITP 2022)},
pages = {10:1--10:19},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-252-5},
issn = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/opus/volltexte/2022/16719},
urn = {urn:nbn:de:0030-drops-167191},
doi = {10.4230/LIPIcs.ITP.2022.10},
annote = {Keywords: Functional analysis, Lean, linear algebra,
semilinear, Hilbert space},
tags = {formalization, lean3}
}
@Article{ EURAM17,
author = {Gabriel Ebner and Sebastian Ullrich and Jared Roesch and
Jeremy Avigad and Leonardo {de Moura}},
title = {A metaprogramming framework for formal verification},
journal = {{PACMPL}},
volume = {1},
number = {{ICFP}},
pages = {34:1--34:29},
year = {2017},
url = {https://doi.org/10.1145/3110278},
doi = {10.1145/3110278},
timestamp = {Tue, 06 Nov 2018 12:51:05 +0100},
biburl = {https://dblp.org/rec/bib/journals/pacmpl/EbnerURAM17},
bibsource = {dblp computer science bibliography, https://dblp.org},
tags = {about-lean, lean3}
}
@Misc{ FernandezMir19,
author = {Ramon Fernández Mir},
title = {Schemes in Lean},
eprint = {https://www.imperial.ac.uk/media/imperial-college/faculty-of-engineering/computing/public/1819-ug-projects/Fernandez-I-MirR-Schemes-in-Lean.pdf},
note = {Project report},
year = {2019},
website = {https://github.com/ramonfmir/lean-scheme},
tags = {formalization, lean3}
}
@Article{ Gouezel2021,
author = {S{\'{e}}bastien Gou{\"{e}}zel},
title = {Formalizing the Gromov-Hausdorff space},
journal = {CoRR},
volume = {abs/2108.13660},
year = {2021},
url = {https://arxiv.org/abs/2108.13660},
eprinttype = {arXiv},
eprint = {2108.13660},
timestamp = {Fri, 03 Sep 2021 10:51:17 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2108-13660.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
tags = {formalization, lean3}
}
@InProceedings{ Gouezel22,
author = {S{\'{e}}bastien Gou{\"{e}}zel},
editor = {Kevin Buzzard and Temur Kutsia},
title = {A Formalization of the Change of Variables Formula for
Integrals in mathlib},
booktitle = {Intelligent Computer Mathematics - 15th International
Conference, {CICM} 2022, Tbilisi, Georgia, September 19-23,
2022, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {13467},
pages = {3--18},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-031-16681-5\_1},
doi = {10.1007/978-3-031-16681-5\_1},
timestamp = {Mon, 19 Sep 2022 18:41:40 +0200},
biburl = {https://dblp.org/rec/conf/mkm/Gouezel22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
tags = {formalization, lean3}
}
@Misc{ GusakovMehtaMiller21,
title = {Formalizing Hall's Marriage Theorem in Lean},
author = {Alena Gusakov and Bhavik Mehta and Kyle A. Miller},
year = {2021},
eprint = {2101.00127},
archiveprefix = {arXiv},
primaryclass = {math.CO},
url = {https://arxiv.org/abs/2101.00127},
tags = {formalization, lean3}
}
@InProceedings{ HanVanDoorn,
author = {Jesse Michael Han and Floris {van Doorn}},
title = {A formal proof of the independence of the continuum
hypothesis},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International
Conference on Certified Programs and Proofs, {CPP} 2020,
New Orleans, LA, USA, January 20-21, 2020},
pages = {353--366},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373826},
doi = {10.1145/3372885.3373826},
timestamp = {Thu, 23 Jan 2020 16:12:31 +0100},
biburl = {https://dblp.org/rec/conf/cpp/HanD20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
website = {https://flypitch.github.io/},
tags = {formalization, lean3}
}
@InProceedings{ HanVanDoorn19,
author = {Jesse Michael Han and Floris {van Doorn}},
title = {A Formalization of Forcing and the Unprovability of the
Continuum Hypothesis},
booktitle = {10th International Conference on Interactive Theorem
Proving, {ITP} 2019, September 9-12, 2019, Portland, OR,
{USA}},
pages = {19:1--19:19},
year = {2019},
crossref = {DBLP:conf/itp/2019},
url = {https://doi.org/10.4230/LIPIcs.ITP.2019.19},
doi = {10.4230/LIPIcs.ITP.2019.19},
timestamp = {Sat, 07 Sep 2019 02:31:13 +0200},
biburl = {https://dblp.org/rec/conf/itp/HanD19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
tags = {formalization, lean3}
}
@Misc{ Huisinga19,
author = {Marc Huisinga},
title = {Formally Verified Insertion of Reference Counting
Instructions},
eprint = {https://pp.ipd.kit.edu/uploads/publikationen/huisinga19bachelorarbeit.pdf},
note = {Bachelor thesis},
year = {2019},
website = {https://github.com/mhuisi/rc-correctness},
tags = {about-lean, lean4}
}
@InCollection{ KjosHanssenNiraulaYoon22,
author = {Kjos-Hanssen, Bj{\o}rn and Niraula, Saroj and Yoon,
Soowhan},
title = {A parametrized family of {T}versky metrics connecting the
{J}accard distance to an analogue of the normalized
information distance},
booktitle = {L{FCS}: Logical foundations of computer science},
series = {Lecture Notes in Comput. Sci.},
publisher = {Springer, [Cham]},
tags = {formalization, lean3},
url = {https://arxiv.org/abs/2111.02498},
year = {2022}
}
@Booklet{ Kudryashov2021,
author = {Yury Kudryashov},
title = {Formalizing Rotation Number and Its Properties in Lean},
howpublished = {EasyChair Preprint no. 6168},
url = {https://easychair.org/publications/preprint/38w1},
year = {2021},
tags = {formalization, lean3}
}
@InProceedings{ Kudryashov22,
author = {Kudryashov, Yury},
title = {{Formalizing the Divergence Theorem and the Cauchy
Integral Formula in Lean}},
booktitle = {13th International Conference on Interactive Theorem
Proving (ITP 2022)},
pages = {23:1--23:19},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-252-5},
issn = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/opus/volltexte/2022/16732},
urn = {urn:nbn:de:0030-drops-167326},
doi = {10.4230/LIPIcs.ITP.2022.23},
annote = {Keywords: divergence theorem, Green’s theorem, Gauge
integral, Cauchy integral formula, Cauchy-Goursat theorem,
complex analysis},
tags = {formalization, lean3}
}
@InProceedings{ LeeHurLopes19,
author = {Juneyoung Lee and Chung{-}Kil Hur and Nuno P. Lopes},
title = {AliveInLean: {A} Verified {LLVM} Peephole Optimization
Verifier},
booktitle = {Computer Aided Verification - 31st International
Conference, {CAV} 2019, New York City, NY, USA, July 15-18,
2019, Proceedings, Part {II}},
pages = {445--455},
year = {2019},
url = "\url{https://doi.org/10.1007/978-3-030-25543-5_25}",
doi = {10.1007/978-3-030-25543-5\_25},
timestamp = {Fri, 27 Mar 2020 08:45:57 +0100},
biburl = {https://dblp.org/rec/conf/cav/LeeHL19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
website = {https://sf.snu.ac.kr/aliveinlean/}
}
@InProceedings{ Lewis17,
author = {Robert Y. Lewis},
title = {An Extensible Ad Hoc Interface between Lean and
Mathematica},
booktitle = {Proceedings of the Fifth Workshop on Proof eXchange for
Theorem Proving, PxTP 2017, Bras{\'{\i}}lia, Brazil, 23-24
September 2017},
pages = {23--37},
year = {2017},
url = {https://doi.org/10.4204/EPTCS.262.4},
doi = {10.4204/EPTCS.262.4},
timestamp = {Wed, 12 Sep 2018 01:05:13 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1712-09288.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
website = {https://robertylewis.com/leanmm/},
tags = {about-mathlib, lean3}
}
@InProceedings{ Lewis19,
author = {Robert Y. Lewis},
title = {A formal proof of {H}ensel's lemma over the p-adic
integers},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International
Conference on Certified Programs and Proofs, {CPP} 2019,
Cascais, Portugal, January 14-15, 2019},
pages = {15--26},
year = {2019},
crossref = {DBLP:conf/cpp/2019},
url = {https://doi.org/10.1145/3293880.3294089},
doi = {10.1145/3293880.3294089},
timestamp = {Fri, 04 Jan 2019 10:46:45 +0100},
biburl = {https://dblp.org/rec/bib/conf/cpp/Lewis19},
bibsource = {dblp computer science bibliography, https://dblp.org},
tags = {formalization, lean3}
}
@InProceedings{ LewisMadelaine20,
author = {Robert Y. Lewis and Paul{-}Nicolas Madelaine},
title = {Simplifying Casts and Coercions},
booktitle = {Practical Aspects of Automated Reasoning, {PAAR} 2020},
year = {2020},
url = {https://arxiv.org/abs/2001.10594},
archiveprefix = {arXiv},
eprint = {2001.10594},
timestamp = {Thu, 30 Jan 2020 18:46:36 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2001-10594.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
tags = {about-mathlib, lean3}
}
@Article{ LewisWu22,
author = {Robert Y. Lewis and Minchao Wu},
title = {A bi-directional extensible interface between Lean and
Mathematica},
journal = {{Journal of Automated Reasoning}},
volume = {66},
number = {1},
year = {2022},
url = {https://robertylewis.com/leanmm/lean_mm.pdf},
website = {https://robertylewis.com/leanmm},
doi = {https://doi.org/10.1007/s10817-021-09611-1},
tags = {about-mathlib, lean3}
}
@InProceedings{ Limperg21,
author = {Limperg, Jannis},
title = {A Novice-Friendly Induction Tactic for Lean},
year = {2021},
isbn = {9781450382991},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3437992.3439928},
doi = {10.1145/3437992.3439928},
abstract = {In theorem provers based on dependent type theory such as
Coq and Lean, induction is a fundamental proof method and
induction tactics are omnipresent in proof scripts. Yet the
ergonomics of existing induction tactics are not ideal:
they do not reliably support inductive predicates and
relations; they sometimes generate overly specific or
unnecessarily complex induction hypotheses; and they
occasionally choose confusing names for the hypotheses they
introduce. This paper describes a new induction tactic,
implemented in Lean 3, which addresses these issues. The
tactic is particularly suitable for educational use, but
experts should also find it more convenient than existing
induction tactics. In addition, the tactic serves as a
moderately complex case study for the metaprogramming
framework of Lean 3. The paper describes some difficulties
encountered during the implementation and suggests
improvements to the framework.},
booktitle = {Proceedings of the 10th ACM SIGPLAN International
Conference on Certified Programs and Proofs},
pages = {199–211},
numpages = {13},
keywords = {induction, Lean, tactic, type theory, metaprogramming},
location = {Virtual, Denmark},
series = {CPP 2021},
tags = {about-mathlib, lean3}
}
@InProceedings{ LimpergF23,
author = {Jannis Limperg and Asta Halkj{\ae}r From},
editor = {Robbert Krebbers and Dmitriy Traytel and Brigitte Pientka
and Steve Zdancewic},
title = {Aesop: White-Box Best-First Proof Search for Lean},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International
Conference on Certified Programs and Proofs, {CPP} 2023,
Boston, MA, USA, January 16-17, 2023},
pages = {253--266},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575671},
doi = {10.1145/3573105.3575671},
tags = {about-mathlib, lean4},
timestamp = {Fri, 13 Jan 2023 13:05:42 +0100},
biburl = {https://dblp.org/rec/conf/cpp/LimpergF23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@InProceedings{ Livingston23,
author = {Livingston, Amelia},
title = {{Group Cohomology in the Lean Community Library}},
booktitle = {14th International Conference on Interactive Theorem
Proving (ITP 2023)},
pages = {22:1--22:17},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-284-6},
issn = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/opus/volltexte/2023/18397},
urn = {urn:nbn:de:0030-drops-183974},
doi = {10.4230/LIPIcs.ITP.2023.22},
annote = {Keywords: formal math, Lean, mathlib, group cohomology,
homological algebra},