Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

/* Wikiproofs */

 'User talk:Kingdon' (rev 2703)
  • Loading branch information...
commit 2b83200d8a00496f8616d31685b7765c36a4e618 1 parent e669a2f
Asalmon14 authored Levitation-perl committed
Showing with 3 additions and 1 deletion.
  1. +3 −1 User talk/K/i/n/Kingdon
View
4 User talk/K/i/n/Kingdon
@@ -156,4 +156,6 @@ Thanks for your pull request. I'm very busy, so I cannot review it right now. So
Hi, I have done some proofs with Metamath's set.mm in the past (many of my shortened proofs are there). I was wondering: does wikiproofs have any advantages over Metamath and friends, besides the fact that it is easily accessible and editable by anyone? Also, more specifically, let's say I had a set and operations that satisfied the axioms for complex numbers. Would I be able to use the complex number module directly, or would I have to create an isomorphism? [[User:Asalmon14|Asalmon14]] ([[User talk:Asalmon14|talk]]) 07:02, 16 May 2012 (UTC)
-:Wikiproofs uses [[Help:JHilbert|JHilbert]], which is like ghilbert in that it aims to solve some of the problems of metamath, while preserving its basic spirit. If you have a module built on set theory which defines +, ·, ℂ, etc, and proves the axioms, you could then export [[Interface:Complex number axioms]] which would then justify an immediate import of [[Interface:Complex numbers]]. An isomorphism would not be necessary or helpful, as far as I can see, because in [[Interface:Complex number axioms]], ℂ is not a particular set; it is either posited to exist (if you take those axioms as axioms), or proven to exist in a module which exports the interface (not in the interface itself). [[User:Kingdon|Kingdon]] ([[User talk:Kingdon|talk]]) 03:21, 17 May 2012 (UTC)
+:Wikiproofs uses [[Help:JHilbert|JHilbert]], which is like ghilbert in that it aims to solve some of the problems of metamath, while preserving its basic spirit. If you have a module built on set theory which defines +, ·, ℂ, etc, and proves the axioms, you could then export [[Interface:Complex number axioms]] which would then justify an immediate import of [[Interface:Complex numbers]]. An isomorphism would not be necessary or helpful, as far as I can see, because in [[Interface:Complex number axioms]], ℂ is not a particular set; it is either posited to exist (if you take those axioms as axioms), or proven to exist in a module which exports the interface (not in the interface itself). [[User:Kingdon|Kingdon]] ([[User talk:Kingdon|talk]]) 03:21, 17 May 2012 (UTC)
+
+::This is definitely an improvement over the Metamath system. You could, no doubt, do the same thing for rings and fields, correct? Unfortunately, I do not know Java, and I probably won't be able to contribute much (I am trying to independent study classes through MIT's Open Courseware in any spare time I can find). If I were given unlimited time, I would certainly want to contribute, and I love working with these automated theorem checkers. [[User:Asalmon14|Asalmon14]] ([[User talk:Asalmon14|talk]]) 01:25, 20 May 2012 (UTC)
Please sign in to comment.
Something went wrong with that request. Please try again.