-
Notifications
You must be signed in to change notification settings - Fork 88
/
mmrecent.raw.html
3363 lines (2809 loc) · 136 KB
/
mmrecent.raw.html
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
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"https://www.w3.org/TR/html4/loose.dtd">
<HTML LANG="EN-US">
<HEAD>
<!-- don't cache this page (i. e. get fresh copy each visit) -->
<META HTTP-EQUIV="EXPIRES" CONTENT="0">
<!-- improve mobile display -->
<META NAME="viewport" CONTENT="width=device-width, initial-scale=1.0">
<META HTTP-EQUIV="Content-Type"
CONTENT="text/html; charset=iso-8859-1">
<STYLE TYPE="text/css">
<!--
.p { font-family: "Arial Narrow";
font-size: x-small;
color: #FA8072;
}
.r { font-family: "Arial Narrow";
font-size: x-small;
}
.i { font-family: "Arial Narrow";
font-size: x-small;
color: gray;
}
/* Math symbol images are shifted down 4 pixels to align with
normal text. All other images must override this shift with
STYLE="margin-bottom:0px" */
img { margin-bottom: -4px }
-->
</STYLE>
<!-- The following section is hard-coded, not automatically generated -->
<STYLE TYPE="text/css">
<!--
.set { color: red; }
.wff { color: blue; }
.class { color: #C3C; }
.symvar { border-bottom:1px dotted;color:#C3C}
.typecode { color: gray }
.hidden { color: gray }
@font-face {
font-family: XITSMath-Regular;
src: url(xits-math.woff);
}
.math { font-family: XITSMath-Regular }
-->
</STYLE>
<LINK href="mmset.css" title="mmset"
rel="stylesheet" type="text/css">
<LINK href="mmsetalt.css" title="mmsetalt"
rel="alternate stylesheet" type="text/css">
<TITLE>Most Recent Proofs - Metamath Proof Explorer</TITLE>
<LINK REL="alternate" TITLE="Metamath RSS"
HREF="http://www.getzdan.com/rss/mmrecent.xml" TYPE="application/rss+xml">
<LINK REL="shortcut icon" HREF="favicon.ico" TYPE="image/x-icon">
</HEAD>
<BODY BGCOLOR="#FFFFFF" STYLE="padding: 0px 8px">
<TABLE BORDER=0 CELLSPACING=0 CELLPADDING=0 WIDTH="100%">
<TR>
<TD ALIGN=LEFT VALIGN=TOP WIDTH="25%"><A HREF="mmset.html"><IMG SRC="mm.gif"
BORDER=0
ALT="Metamath Proof Explorer Home"
TITLE="Metamath Proof Explorer Home"
HEIGHT=32 WIDTH=32 ALIGN=TOP STYLE="margin-bottom:0px"></A>
</TD>
<TD ALIGN=CENTER VALIGN=TOP><FONT SIZE="+3"
COLOR="#006633"><B>Metamath Proof Explorer</B></FONT><BR>
<FONT SIZE="+2" COLOR="#006633"><B>Most Recent Proofs</B>
</FONT>
</TD>
<TD ALIGN=RIGHT VALIGN=TOP WIDTH="25%">
</TD>
</TR>
<TR>
<TD COLSPAN=2 ALIGN=LEFT VALIGN=TOP><FONT SIZE=-2
FACE=sans-serif>
<A HREF="../mm.html">Mirrors</A> >
<A HREF="../index.html">Home</A> >
<A HREF="mmset.html">MPE Home</A> >
<A HREF="mmtheorems.html">Th. List</A> >
Recent
</FONT>
<TD COLSPAN=1 ALIGN=RIGHT VALIGN=TOP><FONT SIZE=-2
FACE=sans-serif>
<A HREF="../ileuni/mmrecent.html">ILE Most Recent</A>
<A HREF="../other.html">Other</A> >
<A HREF="../mm_100.html">MM 100</A>
</FONT>
</TD>
</TR>
</TABLE>
<HR NOSHADE SIZE=1>
<B><FONT COLOR="#006633">Most recent proofs</FONT></B>
These are the
100 (<A HREF="../mpeuni/mmrecent.html#thlist">Unicode</A>,
<A HREF="../mpegif/mmrecent.html#thlist">GIF</A>) or
1000 (<A HREF="../mpeuni/mmrecent1000.html#thlist">Unicode</A>,
<A HREF="../mpegif/mmrecent1000.html#thlist">GIF</A>)
<!--
<A HREF="mmrecent.html#thlist">10</A> or <A
HREF="mmrecent1000.html#thlist">1000</A> (1MB)
-->
most recent proofs in the set.mm database for the Metamath Proof
Explorer (and the Hilbert Space Explorer). The set.mm database is
maintained on GitHub with <A
HREF="https://github.com/metamath/set.mm/tree/master">master</A>
(stable) and <A
HREF="https://github.com/metamath/set.mm/tree/develop">develop</A>
(development) versions. This page was created from
<A HREF="https://github.com/metamath/set.mm/commits/develop">develop
commit 212ee7d9</A>,
also available here: <A HREF="../metamath/set.mm"> set.mm</A>
(43MB) or <A HREF="../metamath/set.mm.bz2">set.mm.bz2</A> (compressed,
13MB).
<!-- -->
<P>The original proofs of theorems with recently shortened proofs can
often be found by appending "OLD" to the theorem name, for example
<A HREF="19.43OLD.html">19.43OLD</A> for <A HREF="19.43.html">19.43</A>.
The "OLD" versions are usually deleted after a year.
<!-- -->
<P>
<!--
The stable set.mm database file in the <A
HREF="../index.html#mmprog">Metamath program download</A> is sometimes
several days behind the preproduction
<A HREF="../metamath/set.mm">
set.mm</A> (17MB) or
<A HREF="../metamath/set.mm.bz2">set.mm.bz2</A>
(compressed, 5MB)
that corresponds to this page.
-->
<B><FONT COLOR="#006633">Other links</FONT></B> Email:
<A HREF="../email.html">Norm Megill</A>.
Mailing list: <A
HREF="http://groups.google.com/group/metamath">Metamath Google Group
<FONT SIZE=-1><I>Updated 7-Dec-2021</I></FONT> </A>.
Contributing: <A HREF="../index.html#contribute">How
can I contribute to Metamath?</A>
Syndication:
<A
HREF="http://www.getzdan.com/rss/mmrecent.xml">RSS feed</A>
<!--
(<A
HREF="http://feeds.feedburner.com/MetamathRecentProofs">web version</A>)
-->
(courtesy of Dan Getz)
<!-- [as of 5-Oct-2019, will be off-line for
about a month]. -->
<!-- (note: the feed URL was changed on
22-Sep-2008). -->
Related wikis:
<!--
<A
HREF="http://wiki.planetmath.org/cgi-bin/wiki.pl/metamath">AsteroidMeta</A>
(<A HREF="http://wiki.planetmath.org/cgi-bin/wiki.pl/RecentChanges">Recent
Changes
</A>);
-->
<!-- off line as of 5-Oct-2019
<A
HREF="http://wikiproofs.org/">Wikiproofs (JHilbert)</A>
(<A HREF="http://wikiproofs.org/w/index.php?title=Special:RecentChanges">Recent
Changes</A>);
-->
<!--
<A HREF="https://sites.google.com/a/ghilbert.org/ghilbert/">Ghilbert site</A>;
-->
<A HREF="http://ghilbert-app.appspot.com">Ghilbert site</A>;
<A HREF="http://groups.google.com/group/ghilbert">Ghilbert
Google Group</A>.
<!-- ;
<A HREF="http://ghilbert-test.appspot.com/wiki">Ghilbert
wiki</A> -->
<!-- <A HREF="http://barghest.ghilbert.org/">Barghest</A> (<A
HREF="http://barghest.ghilbert.org/wiki/RecentChanges">Recent
Changes</A>). -->
<!--
<P><B>Please note that I will not be able to respond to email
from June 28 through July 5.
- Norm</B>
-->
<P><B><FONT COLOR="#006633">Recent news
items</FONT></B>
(7-Aug-2021) Version <A HREF="../index.html#mmprog">0.198</A> of the
metamath program fixes a bug in "write source ... /rewrap" that
prevented end-of-sentence punctuation from appearing in column 79, causing
some rewrapped lines to be shorter than necessary. Because this affects
about 2000 lines in set.mm, you should use version 0.198 or later
for rewrapping before submitting to GitHub.
<P>
(7-May-2021) Mario Carneiro has written a <A
HREF="https://groups.google.com/g/metamath/c/O92B2_w0wNg/m/rJ_fG19LAQAJ">
Metamath verifier in Lean</A>.
<P>
(5-May-2021) Marnix Klooster has written a <A
HREF="https://groups.google.com/g/metamath/c/x52J7yjl5iA/m/fNqTc5bFAQAJ">
Metamath verifier in Zig</A>.
<P>
(24-Mar-2021) Metamath was mentioned in a couple of articles about OpenAI:
<A
HREF="https://venturebeat.com/2021/03/09/researchers-find-that-large-language-models-struggle-with-math/">Researchers
find that large language models struggle with math</A> and <A
HREF="https://analyticsindiamag.com/what-is-gpt-f/">What Is GPT-F?</A>.
<P>
(26-Dec-2020) Version <A HREF="../index.html#mmprog">0.194</A> of the
metamath program adds the keyword "htmlexturl" to the $t comment
to specify external versions of theorem pages. This keyward
has been added to set.mm, and <I>you must update
your local copy of set.mm for "verify markup" to pass
with the new program version.</I><P>
(19-Dec-2020) <A HREF="http://facebook.com/aleksandralekseevichadamov">Aleksandr
A. Adamov</A> has translated the Wikipedia
Metamath page into
<A HREF="https://ru.wikipedia.org/wiki/Metamath">Russian</A>.<P>
(19-Nov-2020) Eric Schmidt's <A
HREF="../other.html#checkmm.cpp">checkmm.cpp</A> was used as a test
case for C'est, "a non-standard version of the C++20 standard library,
with enhanced support for compile-time evaluation." See <A
HREF="https://pkeir.github.io/blog/2020/11/14/cest/">C++20 Compile-time
Metamath Proof Verification using C'est</A>.
<P>
(10-Nov-2020) Filip Cernatescu has updated the <A
HREF="https://www.xpuzzle.co">XPuzzle</A> (Android app) to version 1.2.
XPuzzle is a puzzle with math formulas derived from the Metamath system.
At the bottom of the web page is a link to the Google Play Store, where
the app can be found.<P>
(7-Nov-2020) Richard Penner created a <A
HREF="mmfrege.html">cross-reference guide</A> between Frege's logic
notation and the notation used by set.mm.<P>
(4-Sep-2020) Version <A HREF="../index.html#mmprog">0.192</A> of the
metamath program adds the qualifier '/extract' to 'write source'.
See 'help write source' and also
<A
HREF="https://groups.google.com/g/metamath/c/E08icuHZ_4M/m/7dgrzTNmDAAJ">
this Google Group post</A>.<P>
<!--
(1-Sep-2020) Filip Cernatescu created an Android App called <A
HREF="https://www.xpuzzle.co">XPuzzle</A>, a puzzle with math formulas
derived from the Metamath system. At the bottom of the web page is a
link to the Google Play Store, where the app can be found.<P>
-->
(23-Aug-2020) Version <A HREF="../index.html#mmprog">0.188</A> of the
metamath program adds keywords Conclusion, Fact, Introduction,
Paragraph, Scolia, Scolion, Subsection, and Table to bibliographic
references. See 'help write bibliography' for the complete current
list.<P>
<FONT SIZE=-1><A HREF="#oldernews">Older news...</A></FONT>
<P>
<CENTER>
<TABLE CELLSPACING=0 CELLPADDING=5
SUMMARY="Color key"><TR>
<TD>Color key: </TD><TD BGCOLOR="#EEFFFA" NOWRAP><A
HREF="mmset.html"><IMG SRC="mm.gif" BORDER=0
ALT="Metamath Proof Explorer" HEIGHT=32 WIDTH=32 ALIGN=MIDDLE
STYLE="margin-bottom:0px">
Metamath Proof Explorer</A></TD>
<TD WIDTH=10> </TD>
<TD BGCOLOR="#FAEEFF" NOWRAP><A HREF="mmhil.html"><IMG SRC="atomic.gif"
BORDER=0 ALT="Hilbert Space Explorer" HEIGHT=32 WIDTH=32 ALIGN=MIDDLE
STYLE="margin-bottom:0px">
Hilbert Space Explorer</A></TD>
<TD WIDTH=10> </TD>
<TD BGCOLOR="#FFFFD9" NOWRAP><A HREF="mmtheorems.html#sandbox:bighdr"><IMG
SRC="_sandbox.gif" BORDER=0 ALT="User Mathboxes" HEIGHT=32 WIDTH=32
ALIGN=MIDDLE STYLE="margin-bottom:0px"> User Mathboxes</A></TD>
<TD WIDTH=10> </TD>
</TR></TABLE>
</CENTER>
<!-- <P><CENTER><TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA" F7F7FF FAEEFF -->
<P>
<A NAME="thlist"></A>
<CENTER>
<!-- WRITE RECENT updates a line beginning with a "last updated" comment -->
<!-- last updated -->
</CENTER>
<CENTER>
<TABLE BORDER CELLSPACING=0 CELLPADDING=3 BGCOLOR="#EEFFFA"
SUMMARY="Recent Additions to the Metamath Proof Explorer" WIDTH="100%">
<CAPTION><B>Recent Additions to the Metamath Proof
Explorer</B> <FONT SIZE=-1><A HREF="mmnotes.txt">Notes
(last updated
<!--
<font color=orange>
-->
7-Dec-2020
<!--
</font>
-->
)</A>
<!--
<A HREF="#new">News (last
updated
-->
<!--
<font color=orange>
-->
<!--
19-Jun-12
-->
<!--
</font>
-->
<!--
)</A>
-->
</FONT> </CAPTION>
<TR><TH>Date</TH><TH>Label</TH><TH>Description</TH></TR>
<TR><TH COLSPAN=3>Theorem</TH></TR>
<TR BGCOLOR=white><TD COLSPAN=3><FONT SIZE=-3> </FONT></TD></TR>
<!-- To regenerate the automatically generated content, do the following
in the Metamath program:
metamath
MM> read set.mm
MM> write recent mmrecent.html / count 100
-->
<!-- Start of automatically generated section -->
<!-- do not change the next comment -->
<!-- #START# -->
<!-- #END# -->
<!-- Do not change the preceding comment -->
<!-- End of automatically generated section -->
</TABLE>
</CENTER>
<HR NOSHADE SIZE=1>
<P><B><FONT COLOR="#006633"><A NAME="oldernews"></A>Older news:</FONT></B>
<P>
(29-Jul-2020) Mario Carneiro presented MM0 at the CICM conference. See
<A
HREF="https://groups.google.com/d/msg/metamath/MbFrc9WEIGY/JGnhRp6DAgAJ">
this Google Group post</A> which includes a YouTube link.<P>
(20-Jul-2020) Rohan Ridenour found 5 shorter D-proofs in our <A
HREF="../mmsolitaire/pmproofs.txt">Shortest known proofs...</A> file. In
particular, he reduced *4.39 from 901 to 609 steps. A
note on the <A HREF="../mmsolitaire/mms.html#20-Jul-2020">Metamath
Solitaire</A> page mentions a <A
HREF="https://catsarefluffy.github.io/mmsjs/unify.html">tool</A> that he
worked with.<P>
(19-Jul-2020) David A. Wheeler posted a video (<A
HREF="https://youtu.be/3R27Qx69jHc">https://youtu.be/3R27Qx69jHc</A>) on
how to (re)prove Schwabh�user 4.6 for the Metamath Proof Explorer.
See also his <A HREF="../other.html#dawvideos">older videos</A>.<P>
(19-Jul-2020) In version <A HREF="../index.html#mmprog">0.184</A> of the
metamath program, "verify markup" now checks that mathboxes are
independent i.e. do not cross-reference each other. To turn off this
check, use "/mathbox_skip"<P>
(30-Jun-2020) In version <A HREF="../index.html#mmprog">0.183</A> of the
metamath program, (1) "verify markup" now has checking for (i)
underscores in labels, (ii) that *ALT and *OLD theorems have both
discouragement tags, and (iii) that lines don't have trailing spaces.
(2) "save proof.../rewrap" no longer left-aligns $p/$a comments that
contain the string "<HTML>"; see <A
HREF="https://github.com/metamath/set.mm/pull/1695#issuecomment-652129129">this
note</A>.<P>
(5-Apr-2020) Glauco Siliprandi added a new proof to the <A
HREF="../mm_100.html">100 theorem list</A>, <I>e</I> is Transcendental
<A HREF="etransc.html">etransc</A>, bringing the Metamath total to
74.<P>
(12-Feb-2020) A bug in the 'minimize' command of metamath.exe versions
0.179 (29-Nov-2019) and 0.180 (10-Dec-2019) may incorrectly bring in the
use of new axioms. Version <A HREF="../index.html#mmprog">0.181</A>
fixes it. <P>
<!--
(7-Feb-2020) Filip Cernatescu's <A HREF="../other.html#milp">Milpgame</A> has
been updated to version 1.1a. "I added new features to Milpgame that
are similar to mmj2 features, which I think will be welcome" (see last 3
paragraphs in the "Forward Chaining Strategy" section above). Filip
also uploaded a new tutorial on YouTube, <A
HREF="https://www.youtube.com/watch?v=u5X8EbHUOGs">Milpgame tutorial
3</A>.
<P>
-->
(20-Jan-2020) David A. Wheeler created a video
called
<A HREF="https://www.youtube.com/watch?v=87mnU1ckbI0">
Walkthrough of the tutorial in mmj2</A>. See the
<A HREF="https://groups.google.com/d/msg/metamath/JhFGxCKgb0g/5aEuCvKYCwAJ">
Google Group announcement</A> for more details.
(All of his videos are listed on the <A HREF="../other.html#dawvideos">
Other Metamath-Related Topics</A> page.)<P>
(18-Jan-2020) The <A
HREF="https://www.youtube.com/playlist?list=PLlF-CfQhukNkWwZt45vkNfWfuO-tBBqPN">FOMM
2020 talks</A> are on youtube now. Mario Carneiro's talk is <A
HREF="https://www.youtube.com/watch?v=CqZzbaEuNBs&list=PLlF-CfQhukNkWwZt45vkNfWfuO-tBBqPN&index=18&t=0s">Metamath
Zero, or: How to Verify a Verifier</A>. Since they are washed out in
the video, the <A
HREF="http://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/slides/fomm_carneiro.pdf">PDF
slides</A> are available separately.<P>
<!--
(29-Dec-2019) Filip Cernatescu's <A HREF="../other.html#milp">Milpgame</A> has
been updated to version 0.10. "I reduced the time for syntactic trees
generation and added a feature that finds the rule that fits given requirements
(you enter the statement you want to reach, select the statements to which to
apply the x rule, enter the number of hypotheses of x rule)." Filip also
uploaded a new tutorial on YouTube, <A
HREF="https://www.youtube.com/watch?v=-oRhFBPCMn8">Milpgame 10</A>.
<P>
-->
(14-Dec-2019) Glauco Siliprandi added a new proof to the <A
HREF="../mm_100.html">100 theorem list</A>, Fourier series convergence
<A HREF="fourier.html">fourier</A>, bringing the Metamath total to
73.<P>
(25-Nov-2019) Alexander van der Vekens added a new proof to the <A
HREF="../mm_100.html">100 theorem list</A>,
The Cayley-Hamilton Theorem <A HREF="cayleyhamilton.html">cayleyhamilton</A>,
bringing the Metamath total to 72.<P>
(25-Oct-2019) Mario Carneiro's paper "Metamath Zero: The Cartesian
Theorem Prover" (submitted to CPP 2020) is now available on arXiv: <A
HREF="https://arxiv.org/abs/1910.10703">https://arxiv.org/abs/1910.10703</A>.
There is a related discussion on <A
HREF="https://news.ycombinator.com/item?id=21358674">Hacker News</A>.<P>
(30-Sep-2019) Mario Carneiro's talk about MM0 at <A
HREF="https://itp19.cecs.pdx.edu/">ITP 2019</A> is available on YouTube:
<A HREF="https://youtu.be/7hAShC6K_vA">x86 verification from
scratch</A> (24 minutes). Google Group discussion: <A
HREF="https://groups.google.com/d/msg/metamath/raGj9fO6U2I/BmLGM6xoCgAJ">
Metamath Zero</A>.<P>
(29-Sep-2019) David Wheeler created a fascinating Gource video that
animates the construction of set.mm, available on YouTube: <A
HREF="https://www.youtube.com/watch?v=HWjpq1R828U">Metamath set.mm
contributions viewed with Gource through 2019-09-26</A> (4 minutes).
Google Group discussion: <A
HREF="https://groups.google.com/d/msg/metamath/DqtQCzWbcsM/6EYuD_7cCQAJ">
Gource video of set.mm contributions</A>.<P>
(24-Sep-2019) <A HREF="https://ncatlab.org/nlab/show/HomePage">nLab</A>
added a page for <A
HREF="https://ncatlab.org/nlab/show/Metamath">Metamath</A>. It mentions
Stefan O'Rear's Busy Beaver work using the set.mm axiomatization (and
fails to mention Mario's definitional soundness checker)<P>
<!--
(24-Sep-2019) Metamath references found on the web: (i) <A
HREF="https://ncatlab.org/nlab/show/HomePage">nLab</A> added a page for
<A HREF="https://ncatlab.org/nlab/show/Metamath">Metamath</A>. It
mentions Stefan O'Rear's Busy Beaver work using the set.mm
axiomatization (and fails to mention Mario's definitional soundness
checker). (ii) <A HREF="https://arxiv.org/abs/1905.02718">A Theory of
Particular Sets</A> references the Metamath theorem <A
HREF="iotanul.html">iotanul</A> contributed by Andrew Salmon.
Interestingly, p. 10 shows a "Hilbert-style counterpart" to the <A
HREF="natded.html">natural deduction</A> rule of restricted forall
introduction, which is the closest literature version I've seen to
set.mm's <A HREF="ralrimiv">ralrimiv</A>.<P>
-->
(1-Sep-2019) Xuanji Li published a <A
HREF="../screen1.html#vstudio">Visual Studio Code extension</A> to
support metamath syntax highlighting.<P>
(10-Aug-2019) (revised 21-Sep-2019) Version <A
HREF="../index.html#mmprog">0.178</A> of the metamath program has the
following changes: (1) "minimize_with" will now prevent dependence on
new $a statements unless the new qualifier "/allow_new_axioms" is
specified. For routine usage, it is suggested that you use
"minimize_with * /allow_new_axioms * /no_new_axioms_from ax-*" instead
of just "minimize_with *". See "help minimize_with" and this <A
HREF="https://groups.google.com/d/msg/metamath/f-L91-1jI24/3KJnGa8qCgAJ">Google
Group post</A>. Also note that the qualifier "/allow_growth" has been
renamed to "/may_grow". (2) "/no_versioning" was added to "write
theorem_list".<P>
<!-- Aug. 2020: inactive
(24-Jul-2019) Aleksandr A. Adamov has kindly provided a new
<A HREF="http://ru.metamath.org/">mirror site</A> in Russia.<P>
-->
(8-Jul-2019) Jon Pennant announced the creation of a <A
HREF="https://metamathsearch.herokuapp.com/">Metamath search engine</A>.
Try it and feel free to comment on it at
<A HREF="https://groups.google.com/d/msg/metamath/cTeU5AzUksI/5GesBfDaCwAJ">
https://groups.google.com/d/msg/metamath/cTeU5AzUksI/5GesBfDaCwAJ</A>.<P>
(16-May-2019) Set.mm now has a major new section on <A
HREF="mmtheorems.html#cstrkg">elementary geometry</A>. This begins with
definitions that implement Tarski's axioms of geometry (including
concepts such as congruence and betweenness). This uses set.mm's
extensible structures, making them easier to use for many circumstances.
The section then connects Tarski geometry with geometry in Euclidean
places. Most of the work in this section is due to Thierry Arnoux, with
earlier work by Mario Carneiro and Scott Fenton. [Reported by DAW.]<P>
(9-May-2019) We are sad to report that long-time contributor Alan Sare
passed away on Mar. 23. There is some more information at the top of
his <A HREF="mmtheorems.html#idiALT">mathbox</A> (click on
"Mathbox for Alan Sare") and his <A
HREF="https://docs.google.com/document/d/17PRf-DoKHmzwv_TIdVO1nyKh1NGtQjx_TjPd3xiD9-w/edit#heading=h.gjdgxs">obituary</A>.
We extend our condolences to his family.<P>
(10-Mar-2019) Jon Pennant and Mario Carneiro added a new proof to the <A
HREF="../mm_100.html">100 theorem list</A>,
Heron's formula <A HREF="heron.html">heron</A>,
bringing the Metamath total to 71.<P>
(22-Feb-2019) Alexander van der Vekens added a new proof to the <A
HREF="../mm_100.html">100 theorem list</A>,
Cramer's rule <A HREF="cramer.html">cramer</A>,
bringing the Metamath total to 70.<P>
(6-Feb-2019) David A. Wheeler has made significant improvements and
updates to the <A HREF="../index.html#book"><I>Metamath</I> book</A>.
Any comments, errors found, or suggestions are welcome and should be
turned into an issue or pull request at <A
HREF="https://github.com/metamath/metamath-book">https://github.com/metamath/metamath-book</A>
(or sent to me if you prefer).<P>
(26-Dec-2018) I added <A HREF="mmset.html#oldaxioms">Appendix 8</A>
to the
<A HREF="mmset.html">MPE Home Page</A> that cross-references
new and old axiom numbers.<P>
(20-Dec-2018) The axioms have been renumbered according to this <A
HREF="https://groups.google.com/d/msg/metamath/G1xyJb6RjfI/JSNXPIkVAwAJ">Google
Groups post</A>. <P>
(24-Nov-2018) Thierry Arnoux created a new page on <A
HREF="mmtopstr.html">topological structures</A>. The page along with
its SVG files are maintained on <A
HREF="https://github.com/metamath/set.mm/commits/develop">GitHub</A>.
<P>
(11-Oct-2018) Alexander van der Vekens added a new proof to the <A
HREF="../mm_100.html">100 theorem list</A>,
the Friendship Theorem <A HREF="friendship.html">friendship</A>,
bringing the Metamath total to 69.<P>
(1-Oct-2018) Naip Moro has written <A
HREF="../other.html#gramm">gramm</A>, a
Metamath proof verifier written in Antlr4/Java.<P>
(16-Sep-2018) The definition <A HREF="df-riota.html">df-riota</A>
has been simplified so that it evaluates to the empty set instead
of an Undef value. This change affects a significant part of set.mm.<P>
(2-Sep-2018) Thierry Arnoux added a new proof to the <A
HREF="../mm_100.html">100 theorem list</A>,
Euler's partition theorem <A HREF="eulerpart.html">eulerpart</A>,
bringing the Metamath total to 68.<P>
(1-Sep-2018) The <A HREF="https://kate-editor.org/">Kate editor</A> now
has Metamath <A HREF="../other.html#screen">syntax highlighting</A>
built in. (Communicated by Wolf Lammen.)<P>
(15-Aug-2018) The Intuitionistic Logic Explorer now has a <A
HREF="../ileuni/mmrecent.html">Most Recent Proofs</A> page.<P>
(4-Aug-2018) Version <A HREF="../index.html#mmprog">0.163</A> of the
metamath program now indicates (with an asterisk) which <A
HREF="mmtheorems.html#mmdtoc">Table of Contents</A> headers have
associated comments.<P>
(10-May-2018) George Szpiro,
journalist and author of several books on popular mathematics such as
<I>Poincare's Prize</I> and <I>Numbers Rule</I>, used a genetic
algorithm to find shorter D-proofs of "*3.37" and "meredith" in our <A
HREF="../mmsolitaire/pmproofs.txt">Shortest known proofs...</A> file.<P>
(19-Apr-2018) The <A
HREF="../other.html#emetamath">EMetamath</A> Eclipse plugin has
undergone many improvements since its initial release as the <A
HREF="https://github.com/tirix/Emetamath/blob/master/Emetamath/CHANGES.txt">change
log</A> indicates. Thierry uses it as his main proof assistant and
writes, "I added support for mmj2's auto-transformations, which allows
it to infer several steps when building proofs. This added a lot of
comfort for writing proofs.... I can now switch back and forth between
the proof assistant and editing the Metamath file.... I think no
other proof assistant has this feature."<P>
(11-Apr-2018) Benoît Jubin solved an open problem about
the "<A HREF="mmzfcnd.html#twoness">Axiom of Twoness</A>," showing
that it is necessary for completeness. See
<A HREF="../award2003.html#14">item 14</A> on the
"Open problems and miscellany" page.<P>
(25-Mar-2018) Giovanni Mascellani has announced
<A HREF="../other.html#mmpp">mmpp</A>, a
new proof editing environment for the Metamath language.<P>
(27-Feb-2018) Bill Hale has released an <A
HREF="../other.html#mmapp">app for the Apple iPad and desktop
computer</A> that allows you to browse Metamath theorems and their
proofs.<P>
(17-Jan-2018) Dylan Houlihan has kindly provided a new
<A HREF="http://uk.metamath.org/">mirror site</A>.
He has also provided an rsync server; type "rsync uk.metamath.org::"
in a bash shell
to check its status (it should return "metamath metamath").<P>
(15-Jan-2018) The metamath program, version <A
HREF="../index.html#mmprog">0.157</A>, has been updated to implement
the file inclusion conventions described in the 21-Dec-2017 entry
of <A HREF="mmnotes.txt">mmnotes.txt</A>.<P>
<!--
(26-Dec-2017) At my suggestion, Filip Cernatescu has graciously released
his <A HREF="../other.html#milp">Milpgame 0.5</A> (MILP: Math is like a
puzzle!) as open source under the MIT license on <A
HREF="https://github.com/milpgame">Github</A>, including translating the
source code from Romanian to English. He is eager to hear any feedback
by email or posted to the <A
HREF="https://groups.google.com/d/msg/metamath/mNkv1_oRQho/3a0tfki2AQAJ">Google
group</A>.<P>
-->
(11-Dec-2017) I added a paragraph, suggested by Gérard Lang, to
the distinct variable description <A
HREF="mmset.html#dvexample">here</A>.<P>
(10-Dec-2017) Per FL's request, his mathbox will be removed from set.mm.
If you wish to export any of his theorems, today's version
(<A HREF="https://github.com/metamath/set.mm/commits/master">master
commit 1024a3a</A>) is the last one that will contain it.<P>
(11-Nov-2017) Alan Sare updated his <A
HREF="../other.html#completeusersproof">completeusersproof</A>
program.<P>
(3-Oct-2017) Sean B. Palmer created a <A HREF="../other.html#mmprog">web
page</A> that runs the metamath program under emulated Linux in
JavaScript. He also wrote
<A HREF="https://github.com/sbp/mmm/blob/master/pm.md">some programs </A>
to work with our <A HREF="../other.html#shortest">shortest known proofs
of the PM propositional calculus theorems</A>.<P>
(28-Sep-2017) Ivan Kuckir wrote a tutorial blog entry,
<A HREF="http://blog.ivank.net/introduction-to-metamath.html">Introduction
to Metamath</A>, that summarizes the language syntax.
(It may have been written some time ago, but I was not aware of it
before.)<P>
(26-Sep-2017) The default directory for the Metamath Proof Explorer
(MPE) has been changed from the GIF version (mpegif) to the Unicode
version (mpeuni) throughout the site. Please let me know if you find
broken links or other issues.<P>
(24-Sep-2017) Saveliy Skresanov added a new proof to the <A
HREF="../mm_100.html">100 theorem list</A>,
Ceva's Theorem <A HREF="cevath.html">cevath</A>,
bringing the Metamath total to 67.<P>
(3-Sep-2017) Brendan Leahy added a new proof to the <A
HREF="../mm_100.html">100 theorem list</A>,
Area of a Circle <A HREF="areacirc.html">areacirc</A>,
bringing the Metamath total to 66.<P>
(7-Aug-2017) Mario Carneiro added a new proof to the <A
HREF="../mm_100.html">100 theorem list</A>,
Principle of Inclusion/Exclusion <A HREF="incexc.html">incexc</A>,
bringing the Metamath total to 65.<P>
(1-Jul-2017) Glauco Siliprandi added a new proof to the <A
HREF="../mm_100.html">100 theorem list</A>, Stirling's Formula
<A HREF="stirling.html">stirling</A>,
bringing the Metamath total to 64.
Related theorems include 2 versions
of Wallis' formula for π (<A HREF="wallispi.html">wallispi</A> and
<A HREF="wallispi2.html">wallispi2</A>).<P>
(7-May-2017) Thierry Arnoux added a new proof to the <A
HREF="../mm_100.html">100 theorem list</A>, Betrand's Ballot Problem
<A HREF="ballotth.html">ballotth</A>, bringing the Metamath total to 63.<P>
<!-- 2008
http://science.slashdot.org/comments.pl?sid=981305&cid=25211723
http://science.slashdot.org/comments.pl?sid=981305&cid=25214633
-->
<!--
There is a 24-minute YouTube <A
HREF="https://www.youtube.com/watch?v=YvhRBvMjgvs">demonstration</A>.
-->
<!--
(2-May-2017) In metamath program version <A
HREF="../index.html#mmprog">0.141</A>, this Most Recent Proofs page
(updated by 'write recent_additions') now includes $a as well as $p statements.
-->
(20-Apr-2017) Glauco Siliprandi added a new proof in the
supplementary list on the <A
HREF="../mm_100.html#sup">100 theorem list</A>, Stone-Weierstrass Theorem
<A HREF="stowei.html">stowei</A>.<P>
<!--
<P>(13-Apr-2017) See
<A HREF="equidK.html">equidK</A>
for a discussion of the recent theorems in my mathbox. -NM
-->
(28-Feb-2017) David Moews added a new proof to the <A
HREF="../mm_100.html">100 theorem list</A>, Product of Segments of Chords
<A HREF="chordthm.html">chordthm</A>, bringing the Metamath total to 62.<P>
(1-Jan-2017) Saveliy Skresanov added a new proof to the <A
HREF="../mm_100.html">100 theorem list</A>, Isosceles triangle theorem
<A HREF="isosctr.html">isosctr</A>, bringing the Metamath total to 61.<P>
(1-Jan-2017) Mario Carneiro added 2 new proofs to the <A
HREF="../mm_100.html">100 theorem list</A>, L'Hôpital's Rule
<A HREF="lhop.html">lhop</A>
and Taylor's Theorem
<A HREF="taylth.html">taylth</A>, bringing the Metamath total to 60.<P>
(28-Dec-2016) David A. Wheeler is putting together a page on Metamath
(specifically set.mm) <A HREF="conventions.html">conventions</A>. Comments are
welcome on the Google Group <A
HREF="https://groups.google.com/d/msg/metamath/jTpFJY9V1Ac/Zjip8kBRFQAJ">thread</A>.
<P>(24-Dec-2016) Mario Carneiro introduced the abbreviation "F/ x ph"
(symbols: turned F, x, phi) in
<A HREF="df-nf.html">df-nf</A>
to represent the "effectively not free" idiom "A. x ( ph -> A. x ph )".
Theorem <A HREF="nf2.html">nf2</A> shows a version without nested
quantifiers.
<P>(22-Dec-2016) Naip Moro has developed a <A
HREF="http://naipmoro.github.io/lofmm/">Metamath database</A> for G.
Spencer-Brown's
<A HREF="https://en.wikipedia.org/wiki/Laws_of_Form">Laws of Form</A>.
You can follow the Google Group discussion
<A HREF="https://groups.google.com/d/msg/metamath/Oggn4OWYxK4/6QNO0Jm4EwAJ">here</A>.
<P>(20-Dec-2016) In metamath program version <A
HREF="../index.html#mmprog">0.137</A>, 'verify markup *' now
checks that ax-XXX $a matches axXXX $p
when the latter exists, per the discussion at
<A HREF="https://groups.google.com/d/msg/metamath/Vtz3CKGmXnI/Fxq3j1I_EQAJ">
https://groups.google.com/d/msg/metamath/Vtz3CKGmXnI/Fxq3j1I_EQAJ</A>.
<P>(24-Nov-2016) Mingl Yuan has kindly provided a
<A HREF="http://cn.metamath.org/">mirror site</A> in Beijing,
China. He has also provided an rsync server; type "rsync cn.metamath.org::"
in a bash shell
to check its status (it should return "metamath metamath").
<P>(14-Aug-2016) All HTML pages on this site should now be mobile-friendly
and pass the <A
HREF="https://www.google.com/webmasters/tools/mobile-friendly/">Mobile-Friendly
Test</A>. If you find one that does not, let me know.
<P>(14-Aug-2016) Daniel Whalen wrote a paper describing the use of
using deep learning to prove 14% of test theorems taken from set.mm: <A
HREF="http://arxiv.org/abs/1608.02644">Holophrasm: a neural Automated
Theorem Prover for higher-order logic</A>. The associated program
is called <A HREF="../other.html#holophrasm">Holophrasm</A>.
<P>(14-Aug-2016) David A. Wheeler created a video
called
<A HREF="https://www.youtube.com/watch?v=8WH4Rd4UKGE">
Metamath Proof Explorer: A Modern Principia Mathematica</A>
<P>(12-Aug-2016) A <A HREF="https://gitter.im/metamath/Lobby">Gitter
chat room</A> has been created for Metamath.
<P>(9-Aug-2016) Mario Carneiro wrote a <A
HREF="https://github.com/digama0/mm-scala"> Metamath proof verifier in
the Scala language </A> as part
of the ongoing <A HREF="https://github.com/UniFormal/MMT/pull/176"
>Metamath -> MMT import project</A>
<P>(9-Aug-2016) David A. Wheeler created a GitHub project called <A
HREF="https://github.com/david-a-wheeler/metamath-test">metamath-test</A>
(<A HREF="https://travis-ci.org/david-a-wheeler/metamath-test" >last
execution run</A>) to check that different verifiers both pass good
databases and detect errors in defective ones.
<P>(4-Aug-2016) Mario gave two <A
HREF="../other.html#cicm2016">presentations</A> at CICM 2016.
<P>(17-Jul-2016) Thierry Arnoux has written <A
HREF="../other.html#emetamath">EMetamath</A>, a Metamath plugin for the
Eclipse IDE.
<P>(16-Jul-2016) Mario recovered Chris Capel's
<A HREF="../other.html#displib">collapsible proof demo</A>.
<P>(13-Jul-2016) FL sent me an updated version of <A
HREF="../downloads/inpreima2.pdf">PDF</A> (<A
HREF="../downloads/inpreima2.tex">LaTeX source</A>) developed with
Lamport's <A
HREF="http://research.microsoft.com/en-us/um/people/lamport/latex/pf2.pdf">
pf2</A> package. See the 23-Apr-2012 entry below.
<P>(12-Jul-2016) David A. Wheeler produced a new video for <A
HREF="../index.html#mmj2">mmj2</A> called <A
HREF="https://youtu.be/vE3v175cMKM">"Creating functions in
Metamath"</A>. It shows a more efficient approach than his previous
recent video <A
HREF="https://www.youtube.com/watch?v=vek84PEroIc">"Creating functions
in Metamath" (old)</A> but it can be of interest to see both approaches.
<P>(10-Jul-2016) Metamath program version <A
HREF="../index.html#mmprog">0.132</A> changes the command
'show restricted' to 'show discouraged' and adds a new command,
'set discouragement'. See the <A HREF="mmnotes.txt">mmnotes.txt</A> entry of
11-May-2016 (updated 10-Jul-2016).
<P>(12-Jun-2016) Dan Getz has written <A
HREF="https://github.com/getzdan/Metamath.jl">Metamath.jl</A>, a
Metamath proof verifier written in the <A
HREF="https://en.wikipedia.org/wiki/Julia_(programming_language)">Julia</A>
language.
<P>(10-Jun-2016) If you are using metamath program versions
0.128, 0.129, or 0.130, please update to version <A
HREF="../index.html#mmprog">0.131</A>. (In the bad versions,
'minimize_with' ignores distinct variable violations.)
<P>(1-Jun-2016) Mario Carneiro added new proofs to the <A
HREF="../mm_100.html">100 theorem list</A>, the Prime Number Theorem
<A HREF="pnt.html">pnt</A> and the
Perfect Number Theorem <A HREF="perfect.html">perfect</A>,
bringing the Metamath total to 58.
<P>(12-May-2016) Mario Carneiro added a new proof to the <A
HREF="../mm_100.html">100 theorem list</A>, Dirichlet's theorem
<A HREF="dirith.html">dirith</A>, bringing the Metamath total to 56.
(Added 17-May-2016) An informal exposition of the proof can be found at
<A HREF="http://metamath-blog.blogspot.com/2016/05/dirichlets-theorem.html">
http://metamath-blog.blogspot.com/2016/05/dirichlets-theorem.html</A>
<P>(10-Mar-2016) Metamath program version <A
HREF="../index.html#mmprog">0.125</A> adds a new qualifier, /fast, to
'save proof'. See the <A HREF="mmnotes.txt">mmnotes.txt</A> entry of
10-Mar-2016.
<P>(6-Mar-2016) The most recent set.mm has a large update converting
variables from letters to symbols. See <A
HREF="https://groups.google.com/d/msg/metamath/w3f1cVH3R_g/0fO1hnIOBQAJ">
this Google Groups post</A>.
<P>(16-Feb-2016) Mario Carneiro's new paper
"Models for Metamath" can
be found <A HREF="../ocat/model/model.pdf">here</A> and
on <A HREF="http://arxiv.org/abs/1601.07699">arxiv.org</A>.
<P>(6-Feb-2016) There are now 22 math symbols that can be used as variable
names. See <A HREF="mmascii.html">mmascii.html</A> near the 50th table
row, starting with "./\".
<!-- We are
still trying to decide on a generic way to distinguish them from ordinary
symbols by some means other than color (for those who are color blind
and for printing
unambiguously in black
and white). The page <A
HREF="../mpeuni/mmtheorems271.html">mmtheorems271</A> shows examples of
the use of these symbols. In the current experiment, a dotted underline is
the default, and to compare a dotted
box (on mpeuni pages), use View -> Page Sytle -> mmsetalt (Firefox) or
View -> Style -> mmsetalt (IE).
-->
<!--
<BR> • We note that the first use of colored
symbols as variables was by FL in 2010. See for example theorem <A
HREF="vecax4.html">vecax4</A>.
-->
<P>(29-Jan-2016)
Metamath program version <A
HREF="../index.html#mmprog">0.123</A> adds /packed and /explicit
qualifiers to 'save proof' and 'show proof'. See
<A HREF="https://groups.google.com/d/msg/metamath/xCUNA2ttHew/RXSNzdovBAAJ">
this Google Groups post</A>.
<P>(13-Jan-2016) The Unicode math symbols now provide for external CSS and
use the XITS web font. Thanks to
David A. Wheeler, Mario Carneiro, Cris Perdue, Jason Orendorff,
and Frédéric Liné for discussions on this
topic. Two commands, htmlcss and htmlfont, were added to the
$t comment in set.mm and are recognized by
Metamath program version <A
HREF="../index.html#mmprog">0.122</A>.
<P>(21-Dec-2015) Axiom ax-12, now renamed <A HREF="ax-12o.html">ax-12o</A>,
was replaced by a new shorter equivalent, <A
HREF="ax-12.html">ax-12</A>. The equivalence is provided by theorems <A
HREF="ax12o.html">ax12o</A> and <A HREF="ax12.html">ax12</A>.
<!-- To better
isolate some of the axiomatics, I added a new axiom, <A
HREF="ax-9v.html">ax-9v</A>, which is <A HREF="ax-9.html">ax-9</A>
weakened with a $d. It is used to derive the 3 theorems <A
HREF="ax12o.html">ax12o</A>, <A HREF="ax9.html">ax10</A>, and <A
HREF="ax9.html">ax10</A> in that order since each depends on the
previous. Axiom