M.P.E. Home
Theorem List
Metamath Home
Most Recent Proofs
| M.P.E. Home
Theorem List Metamath Home |
Metamath Proof
Explorer
Most Recent Proofs | A theorem a day prevents mental decay. —mathematician Eric Charles Milner (1928-1997) |
Some users have reported that they cannot always access this page, apparently because port 8888 is sometimes mysteriously blocked. I added two other ports, and this page can now be accessed via ports 88, 443, and 8888. You can discuss this problem here. — Norm 24 Jun 2008
| Color key: |
Metamath Proof Explorer |
Hilbert Space Explorer
(and user's sandboxes at the end) |
| Date | Label | Description |
|---|---|---|
| Theorem | ||
| 6-Jul-2008 | lmbrnns 7905 | Express the binary relation "sequence F converges to point P " in a metric space." |
| ⊢ X = dom dom D & ⊢ (k ∈ ℕ → A = (F ‘k)) ⇒ ⊢ ((D ∈ Met ⋀ P ∈ X ⋀ F:ℕ–→X) → (F(⇝m ‘D)P ↔ ∀x ∈ ℝ+ ∃j ∈ ℕ ∀k ∈ ℕ (j ≤ k → (ADP) < x))) | ||
| 5-Jul-2008 | pjocco 10078 | Composition of projections of a subspace and its orthocomplement. |
| ⊢ H ∈ Cℋ ⇒ ⊢ ((proj ‘H) ∘ (proj ‘(⊥ ‘H))) = 0hop | ||
| 5-Jul-2008 | leoptrt 10042 | The positive operator ordering relation is transitive. Exercise 1(iv) of [Retherford] p. 49. |
| ⊢ (((S ∈ HrmOp ⋀ T ∈ HrmOp ⋀ U ∈ HrmOp) ⋀ (S ≤op T ⋀ T ≤op U)) → S ≤op U) | ||
| 5-Jul-2008 | iscau4 7903 | Express the property "F is a Cauchy sequence of metric D." |
| ⊢ X = dom dom D ⇒ ⊢ (D ∈ Met → (F ∈ (Cau ‘D) ↔ (F ⊆ (ℂ × X) ⋀ ∀x ∈ ℝ (0 < x → ∃j ∈ ℤ ∀k ∈ ℤ (j ≤ k → ((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < x)))))) | ||
| 4-Jul-2008 | bracnlnvalt 10019 | The vector that a continuous linear functional is the bra of. |
| ⊢ (T ∈ (LinFn ∩ ConFn) → T = (bra ‘∪{y ∈ ℋ ∣∀x ∈ ℋ (T ‘x) = (x ·ih y)})) | ||
| 3-Jul-2008 | unisn3 2875 | Union of a singleton in the form of a restricted class abstraction. |
| ⊢ (A ∈ B → ∪{x ∈ B∣x = A} = A) | ||
| 2-Jul-2008 | nmopcoadj0 10008 | An operator composed with its adjoint is zero iff the operator is zero. Theorem 3.11(vii) of [Beran] p. 106. |
| ⊢ T ∈ BndLinOp ⇒ ⊢ ((T ∘ (adjh ‘T)) = 0hop ↔ T = 0hop ) | ||
| 2-Jul-2008 | sylancom 472 | Syllogism inference with commutation of antecents. |
| ⊢ ((φ ⋀ ψ) → χ) & ⊢ ((χ ⋀ ψ) → θ) ⇒ ⊢ ((φ ⋀ ψ) → θ) | ||
| 1-Jul-2008 | supmax 4580 | The greatest element of a set is the supremum. Note that the converse is not true; the supremum might not be an element of the set considered. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
| ⊢ R Or A ⇒ ⊢ ((C ∈ A ⋀ C ∈ B ⋀ ∀y ∈ B ¬ CRy) → sup(B, A, R) = C) | ||
| 1-Jul-2008 | supmaxlem 4579 | A set that contains a greatest element satisfies the antecedent in supremum theorems. This allows sup(A, B, R) to be used in some situations without the completeness axiom. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
| ⊢ ((C ∈ A ⋀ C ∈ B ⋀ ∀z ∈ B ¬ CRz) → ∃x ∈ A (∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz))) | ||
(23-May-2008) Gérard Lang pointed me to Bob Solovay's note on AC and strongly inaccessible cardinals. One of the eventual goals for set.mm is to prove the Axiom of Choice from Grothendieck's axiom, like Mizar does, and this note may be helpful for anyone wanting to attempt that. Separately, I also came across a history of the size reduction of grothprim (viewable in Firefox and some versions of Internet Explorer).
(14-Apr-2008) A "/join" qualifier was added to the "search" command in the metamath program (version 0.07.37). This qualifier will join the $e hypotheses to the $a or $p for searching, so that math tokens in the $e's can be matched as well. For example, "search *com* +v" produces no results, but "search *com* +v /join" yields commutative laws involving vector addition. Thanks to Stefan Allan for suggesting this idea.
(8-Apr-2008) The 8,000th theorem, hlrel, was added to the Metamath Proof Explorer part of the database.
(2-Mar-2008) I added a small section to the end of the Deduction Theorem page.
(17-Feb-2008) ocat has uploaded the "1-Mar-2008" mmj2: mmj2.zip. See the description.
(16-Jan-2008) O'Cat has written mmj2 Proof Assistant Quick Tips.
(30-Dec-2007) "How to build a library of formalized mathematics".
(22-Dec-2007) The Metamath Proof Explorer was included in the top 30 science resources for 2007 by the University at Albany Science Library.
(17-Dec-2007) Metamath's Wikipedia entry says, "This article may require cleanup to meet Wikipedia's quality standards" (see its discussion page). Volunteers are welcome. :) (In the interest of objectivity, I don't edit this entry.)
(20-Nov-2007) Jeff Hoffman created nicod.mm and posted it to the Google Metamath Group.
(19-Nov-2007) Reinder Verlinde suggested adding tooltips to the hyperlinks on the proof pages, which I did for proof step hyperlinks. Discussion.
(5-Nov-2007) A Usenet challenge. :)
(4-Aug-2007) I added a "Request for comments on proposed 'maps to' notation" at the bottom of the AsteroidMeta set.mm discussion page.
(21-Jun-2007) A preprint (PDF file) describing Kurt Maes' axiom of choice with 5 quantifiers, proved in set.mm as ackm.
(20-Jun-2007) The 7,000th theorem, ifpr, was added to the Metamath Proof Explorer part of the database.
(29-Apr-2007) Blog mentions of Metamath: here and here.
(21-Mar-2007) Paul Chapman is working on a new proof browser, which has highlighting that allows you to see the referenced theorem before and after the substitution was made. Here is a screenshot of theorem 0nn0 and a screenshot of theorem 2p2e4.
(15-Mar-2007) A picture of Penny the cat guarding the us2.metamath.org:8888 server and making the rounds.
(16-Feb-2007) For convenience, the program "drule.c" (pronounced "D-rule", not "drool") mentioned in pmproofs.txt can now be downloaded (drule.c) without having to ask me for it. The same disclaimer applies: even though this program works and has no known bugs, it was not intended for general release. Read the comments at the top of the program for instructions.
(28-Jan-2007) Jason Orendorff set up a new mailing list for Metamath: http://groups.google.com/group/metamath.
(20-Jan-2007) Bob Solovay provided a revised version of his Metamath database for Peano arithmetic, peano.mm.
(2-Jan-2007) Raph Levien has set up a wiki called Barghest for the Ghilbert language and software.
(26-Dec-2006) I posted an explanation of theorem ecoprass on Usenet.
(2-Dec-2006) Berislav Žarnić translated the Metamath Solitaire applet to Croatian.
(26-Nov-2006) Dan Getz has created an RSS feed for new theorems as they appear on this page.
(6-Nov-2006) The first 3 paragraphs in Appendix 2: Note on the Axioms were rewritten to clarify the connection between Tarski's axiom system and Metamath.
(31-Oct-2006) ocat asked for a do-over due to a bug in mmj2 -- if you downloaded the mmj2.zip version dated 10/28/2006, then download the new version dated 10/30.
(29-Oct-2006) ocat has announced that the
long-awaited 1-Nov-2006 release of mmj2 is available now.
The new "Unify+Get Hints" is quite
useful, and any proof can be generated as follows. With "?" in the Hyp
field and Ref field blank, select "Unify+Get Hints". Select a hint from
the list and put it in the Ref field. Edit any $n dummy variables to
become the desired wffs. Rinse and repeat for the new proof steps
generated, until the proof is done.
The new tutorial, mmj2PATutorial.bat,
explains this in detail. One way to reduce or avoid dummy $n's is to
fill in the Hyp field with a comma-separated list of any known
hypothesis matches to earlier proof steps, keeping a "?" in the list to
indicate that the remaining hypotheses are unknown. Then "Unify+Get
Hints" can be applied. The tutorial page
\mmj2\data\mmp\PATutorial\Page405.mmp has an example.
Don't forget that the eimm
export/import program lets you go back and forth between the mmj2 and
the metamath program proof assistants, without exiting from either one,
to exploit the best features of each as required.
(21-Oct-2006) Martin Kiselkov has written a Metamath proof verifier in the Lua scripting language, called verify.lua. While it is not practical as an everyday verifier - he writes that it takes about 40 minutes to verify set.mm on a a Pentium 4 - it could be useful to someone learning Lua or Metamath, and importantly it provides another independent way of verifying the correctness of Metamath proofs. His code looks like it is nicely structured and very readable. He is currently working on a faster version in C++.
(19-Oct-2006) New AsteroidMeta page by Raph, Distinctors_vs_binders.
(13-Oct-2006) I put a simple Metamath browser on my PDA (Palm Tungsten E) so that I don't have to lug around my laptop. Here is a screenshot. It isn't polished, but I'll provide the file + instructions if anyone wants it.
(3-Oct-2006) A blog entry, Principia for Reverse Mathematics.
(28-Sep-2006) A blog entry, Metamath responds.
(26-Sep-2006) A blog entry, Metamath isn't hygienic.
(11-Aug-2006) A blog entry, Metamath and the Peano Induction Axiom.
(26-Jul-2006) A new open problem in predicate calculus was added.
(18-Jun-2006) The 6,000th theorem, mt4d, was added to the Metamath Proof Explorer part of the database.
(9-May-2006) Luca Ciciriello has upgraded the t2mf program, which is a C
program used to create the MIDI files on the
Metamath Music Page, so
that it works on MacOS X. This is a nice accomplishment, since the
original program was written before C was standardized by ANSI and will
not compile on modern compilers.
Unfortunately, the original program source states no copyright terms.
The main author, Tim Thompson, has kindly agreed to release his code to
public domain, but two other authors have also contributed to the code,
and so far I have been unable to contact them for copyright clearance.
Therefore I cannot offer the MacOS X version for public download on this
site until this is resolved. Update 10-May-2006: Another author,
M. Czeiszperger, has released his contribution to public domain.
If you are interested in Luca's modified source code,
please contact me directly.
(18-Apr-2006) Incomplete proofs in progress can now be interchanged between the Metamath program's CLI Proof Assistant and mmj2's GUI Proof Assistant, using a new export-import program called eimm. This can be done without exiting either proof assistant, so that the strengths of each approach can be exploited during proof development. See "Use Case 5a" and "Use Case 5b" at mmj2ProofAssistantFeedback.
(28-Mar-2006) Scott Fenton updated his second version of Metamath Solitaire (the one that uses external axioms). He writes: "I've switched to making it a standalone program, as it seems silly to have an applet that can't be run in a web browser. Check the README file for further info." The download is mmsol-0.5.tar.gz.
(27-Mar-2006) Scott Fenton has updated the Metamath Solitaire Java
applet to Java 1.5: (1) QSort has been stripped out: its functionality
is in the Collections class that Sun ships; (2) all Vectors have been
replaced by ArrayLists; (3) generic types have been tossed in wherever
they fit: this cuts back drastically on casting; and (4) any warnings
Eclipse spouted out have been dealt with. I haven't yet updated it
officially, because I don't know if it will work with Microsoft's JVM in
older versions of Internet Explorer. The current official version is
compiled with Java 1.3, because it won't work with Microsoft's JVM if it
is compiled with Java 1.4. (As distasteful as that seems,
I will get complaints from users if it
doesn't work with Microsoft's JVM.) If anyone can verify that Scott's new
version runs on Microsoft's JVM, I would be grateful. Scott's new
version is mm.java-1.5.gz; after
uncompressing it, rename it to mm.java,
use it to replace the existing mm.java file in the
Metamath Solitaire download, and recompile according to instructions
in the mm.java comments.
Scott has also created a second version, mmsol-0.2.tar.gz, that reads
the axioms from ASCII files, instead of having the axioms hard-coded in
the program. This can be very useful if you want to play with custom
axioms, and you can also add a collection of starting theorems as
"axioms" to work from. However, it must be run from the local directory
with appletviewer, since the default Java security model doesn't allow
reading files from a browser. It works with the JDK 5 Update 6
Java download.
To compile (from Windows Command Prompt): C:\Program
Files\Java\jdk1.5.0_06\bin\javac.exe mm.java
To run (from Windows Command Prompt): C:\Program
Files\Java\jdk1.5.0_06\bin\appletviewer.exe mms.html
(21-Jan-2006) Juha Arpiainen proved the independence of axiom ax-11 from the others. This was published as an open problem in my 1995 paper (Remark 9.5 on PDF page 17). See Item 9a on the Workshop Miscellany for his seven-line proof. See also the Asteroid Meta metamathMathQuestions page under the heading "Axiom of variable substitution: ax-11". Congratulations, Juha!
(20-Oct-2005) Juha Arpiainen is working on a proof verifier in Common Lisp called Bourbaki. Its proof language has its roots in Metamath, with the goal of providing a more powerful syntax and definitional soundness checking. See its documentation and related discussion.
(17-Oct-2005) Marnix Klooster has written a Metamath proof verifier in Haskell, called Hmm. Also see his Announcement. The complete program (Hmm.hs, HmmImpl.hs, and HmmVerify.hs) has only 444 lines of code, excluding comments and blank lines. It verifies compressed as well as regular proofs; moreover, it transparently verifies both per-spec compressed proofs and the flawed format he uncovered (see comment below of 16-Oct-05).
(16-Oct-2005) Marnix Klooster noticed that for large proofs, the compressed proof format did not match the spec in the book. His algorithm to correct the problem has been put into the Metamath program (version 0.07.6). The program still verifies older proofs with the incorrect format, but the user will be nagged to update them with 'save proof *'. In set.mm, 285 out of 6376 proofs are affected. (The incorrect format did not affect proof correctness or verification, since the compression and decompression algorithms matched each other.)
(13-Sep-2005) Scott Fenton found an interesting axiom, ax46, which could be used to replace both ax-4 and ax-6.
(29-Jul-2005) Metamath was selected as site of the week by American Scientist Online.
(8-Jul-2005) Roy Longton has contributed 53 new theorems to the Quantum Logic Explorer. You can see them in the Theorem List starting at lem3.3.3lem1. He writes, "If you want, you can post an open challenge to see if anyone can find shorter proofs of the theorems I submitted."
(10-May-2005) A Usenet post I posted about the infinite prime proof; another one about indexed unions.
(3-May-2005) The theorem divexpt is the 5,000th theorem added to the Metamath Proof Explorer database.
(12-Apr-2005) Raph Levien solved the open problem in item 16 on the Workshop Miscellany page and as a corollary proved that axiom ax-9 is independent from the other axioms of predicate calculus and equality. This is the first such independence proof so far; a goal is to prove all of them independent (or to derive any redundant ones from the others).
(8-Mar-2005) I added a paragraph above our complex number axioms table, summarizing the construction and indicating where Dedekind cuts are defined. Thanks to Andrew Buhr for comments on this.
(16-Feb-2005) The Metamath Music Page is mentioned as a reference or resource for a university course called Math, Mind, and Music. .
(28-Jan-2005) Steven Cullinane parodied the Metamath Music Page in his blog.
(18-Jan-2005) Waldek Hebisch upgraded the Metamath program to run on the AMD64 64-bit processor.
(17-Jan-2005) A symbol list summary was added to the beginning of the Hilbert Space Explorer Home Page. Thanks to Mladen Pavicic for suggesting this.
(6-Jan-2005) Someone assembled an amazon.com list of some of the books in the Metamath Proof Explorer Bibliography.
(4-Jan-2005) The definition of ordinal exponentiation was decided on after this Usenet discussion.
(19-Dec-2004) A bit of trivia: my Erdös number is 2, as you can see from this list.
(20-Oct-2004) I started this Usenet discussion about the "reals are uncountable" proof (127 comments; last one on Nov. 12).
(12-Oct-2004) gch-kn shows the equivalence of the Generalized Continuum Hypothesis and Prof. Nambiar's Axiom of Combinatorial Sets. This proof answers his Open Problem 2 (PDF file).
(5-Aug-2004) I gave a talk on "Hilbert Lattice Equations" at the Argonne workshop.
(25-Jul-2004) The theorem nthruz is the 4,000th theorem added to the Metamath Proof Explorer database.
(27-May-2004) Josiah Burroughs contributed the proofs u1lemn1b, u1lem3var1, oi3oa3lem1, and oi3oa3 to the Quantum Logic Explorer database ql.mm.
(23-May-2004) Some minor typos found by Josh Purinton were corrected in the Metamath book. In addition, Josh simplified the definition of the closure of a pre-statement of a formal system in Appendix C.
(5-May-2004) Gregory Bush has found shorter proofs for 67 of the 193 propositional calculus theorems listed in Principia Mathematica, thus establishing 67 new records. (This was challenge #4 on the open problems page.)
| Copyright terms: Public domain | W3C HTML validation [external] |
