Peer Review for material titled "Metamath Solitaire"
eTextbook Reviews for material titled "Metamath Solitaire"
User Rating for material titled "Metamath Solitaire"
Member Comments for material titled "Metamath Solitaire"
Bookmark Collections for material titled "Metamath Solitaire"
Course ePortfolios for material titled "Metamath Solitaire"
Learning Exercises for material titled "Metamath Solitaire"
Accessibility Info for material titled "Metamath Solitaire"
Please enter a Bookmark title
Please limit Bookmark title to 65 characters
Please enter a description
Please limit Bookmark title to 4000 characters
A Bookmark with this title already existed.
Please limit a note about this material to 2048 characters
Search all MERLOT
Select to go to your profile
Select to go to your workspace
Select to go to your Dashboard Report
Select to go to your Content Builder
Select to log out
Search Terms
Enter username
Enter password
Please give at least one keyword of at least three characters for the search to work with. The more keywords you give, the better the search will work for you.
Select OK to launch help window
Cancel help


Advanced Search


Search > Material Results >

Metamath Solitaire


Metamath Solitaire

Logo for Metamath Solitaire
This applet lets you build simple mathematical proofs from axioms in logic and set theory.
Go to material
Material Type: Simulation
Date Added to MERLOT: July 21, 1997
Date Modified in MERLOT: November 27, 2016
Send email to


  • Reviewed by members of Editorial board for inclusion in MERLOT.
    Editor Review
    Very good quality; in queue to be peer reviewed
    avg: 5 rating
  • User review 4.67 average rating
  • User Rating: 4.67 user rating
  • Discussion (2 Comments)
  • Learning Exercises (none)
  • Bookmark Collections (none)
  • Course ePortfolios (none)
  • Accessibility Info (none)

  • Rate this material
  • Create a learning exercise
  • Add accessibility information
  • Pick a Bookmark Collection or Course ePortfolio to put this material in or scroll to the bottom to create a new Bookmark Collection
    Name the Bookmark Collection to represent the materials you will add
    Describe the Bookmark Collection so other MERLOT users will know what it contains and if it has value for their work or teaching. Other users can copy your Bookmark Collection to their own profile and modify it to save time.
    Edit the information about the material in this {0}
    Submitting Bookmarks...


Primary Audience: College General Ed
Mobile Compatibility: Not specified at this time
Language: English
Cost Involved: no
Source Code Available: yes
Accessibility Information Available: no
Creative Commons: unsure


QR Code for this Page

Users who viewed this material also viewed...


Discussion for Metamath Solitaire

Log in to participate in the discussions or Sign up if you are not already a MERLOT member.

Return to Top of Page
Avatar for Amr Sharaf
8 years ago

Amr Sharaf (Faculty)

I will use the material in discrete math class, as reference for Math logic. The proofs are very clear
Used in course

Avatar for Kannan Nambiar
13 years ago

Kannan Nambiar (Faculty)

Many scientists believe in, what is called pantheism, the idea that the complex
working of the nature around us is the only palpable God we can deal with. For
this reason, Reality is the name used by philosophers to discuss God, so that
the highly emotional content that goes with the word God can be avoided. From
this it should be clear that reality is the same as metamathematics. Most
philosophers agree that contemplation of Reality is the highest form of
happiness. So, if you want happiness, play Metamath Solitaire all by yourself.

Technical Remarks:

The applet Metamath Solitaire lets you build simple mathematical proofs from
axioms in logic and set theory. This applet is based on a program called
Metamath, which can express theorems in abstract mathematics, accompanied by
proofs that can be verified by a computer program. Looking at Metamath, confirms
many of my beliefs. Beauty, simplicity, and rigor are the same. You can trust a
computer more than a mathematician. You must accept the four color conjecture,
instead of quibbling about it. All proofs of all mathematics can be arranged in
the lexical order in The Book, the amount of paper available being the only
limitation (see White Hole, Black Whole and The Book, in Merlot, Foundations of
Mathematics).This means that you can read The Book and collect as many theorems
as you want, but don't ask for a solution to your conjecture. There is no good
mathematics that a good high school student cannot understand. Any problem which
has a solution, has a simple solution. It is not enough to define empty set,
you must define the Void, when not even the empty set is there, of course, Void
is not a set, but we need the name. If we have Void, we can call a Dedekind cut
a Void. If we have Void, we can answer the uncomfortable question, What was
there before the Big Bang?, the answer is of course Void. It is not enough to
define cardinals, we want the Absolute, which contains all the cardinals. Of
course, Absolute is not a set (fortunately for us, Cantor has accepted this