2006 JMM
=What?= Page for general strategies and discussion having to do with [http://www.ams.org/amsmtgs/2095_intro.html . . . We are presenting two PM/AM related talks, * [[Metamathematical Visions - metadata, learning, and . . . that I think could gel up to a section of the "metamathematical visions" talk. --[[jcorneli]] ---- . . .
3K - last updated 2006-01-16 16:35 UTC by jcorneli
2006 PM Summer of Code Coordination
Back to [[PM_Summers_of_Code|main PM SoC page]]. = Intro = Are you a student? Do you want to help out . . . ([[The Free Encyclopedia of Mathematics]]) * metamathematics/linguistics/AI track(s) ([[The Hyperreal . . .
6K - last updated 2006-05-29 04:46 UTC by akrowne
2008 PM Summer of Code Coordination
Back to [[PM_Summers_of_Code|main PM SoC page]]. Up to [[SoC metapage]]. = Intro = Are you a student? . . . don't know if anyone other than the Friends Of Metamath read this wiki...) --[[ocat]] Hi, I am interested . . .
18K - last updated 2008-07-05 23:44 UTC by akrowne
43
This is an obscene spammer. This wiki seems to be filling up with people who make up random usernames . . . working together. I appreciate you hosting the Metamath and Ghilbert discussion, so maybe this is . . .
1K - last updated 2007-01-10 17:05 UTC by raph
A metamath bug
*Final disposition: Behavior by design, not a bug.* There is perhaps a problem when you type sh p hbex. . . .
2K - last updated 2006-04-22 16:18 UTC by norm
A note from some members of PlanetMath who dislike this media
==A note from some members of PlanetMath who dislike this media== This page is created as a reaction . . . Ocat and Norm might regard PM as periheral and metamath as central. As for me, I like having a periphery . . . non-PM discussions is beneficial for Friends of Metamath and HDM... ...I remember way, way back in . . . with nearly a dozen software works related to Metamath submitted by people all over the world. And . . . inventions, such as the Earley Parser and the Metamath Proof Verification algorithm. But a lot of . . .
19K - last updated 2007-04-05 15:07 UTC by jcorneli
Asteroid Bulletin for the week of April 10 2005
= This week's big doings = ; development of template utilities continued : http://oddwiki.taoriver.net/wiki.pl/AsteroidMeta/template_utilities . . . Sun Apr 10 06:46:35 2005 UTC Since the metamath website contains a bunch of theorems from . . .
4K - last updated 2005-05-05 04:23 UTC by planetx.cc.vt.edu
Asteroid Bulletin for the week of April 17 2005
=Possible topics for essays= * Getting letters of support for grants * Discussion of [[nested noosphere . . . checking proofs in propositional logic from the metamath website (http://us.metamath.org/mpegif/mmtheorems.html). . . .
4K - last updated 2005-05-05 04:23 UTC by planetx.cc.vt.edu
Asteroid Bulletin for the week of April 3 2005
=Welcome!= Welcome to the first edition of the Asteroid Bulletin. This will be a weekly chronicle sent . . . for doing substitution. If you're interested in metamathematics or computer math, you might want to . . .
6K - last updated 2005-05-05 04:24 UTC by planetx.cc.vt.edu
Asteroid Bulletin for the week of May 1 2005
=Op Ed: Happy May Day!= Writers of the world unite... you have nothing to lose but your fences... and . . . to read in the proofs from the !TeX file for the metamath proof explorer, automatically translate them . . .
16K - last updated 2006-03-22 21:12 UTC by jcorneli
Asteroid Bulletin for the week of May 22 2005
=Letter from the editor= Hi folks, its been a busy week on the Asteroid, but no one has taken the time . . . you might check out the mathematical-metamathematics stuff Ray has been working on: What_is_a_Mathematical_Entity . . .
3K - last updated 2005-05-24 21:07 UTC by jcorneli
Barghest
Update 2006-01-06: Thanks to work by [[dan]], development has now shifted over to the Django framework . . . be one web page per theorem, just like the [[Metamath]] proof explorer. Like Metamath, the terms . . . there are to be major differences. While the Metamath site is read-only, virtually all of the content . . . analysis. You can see it at file: ./mmj2/doc/MetamathERNotes.html in the mmj2.zip download. That . . . invent a Unification algorithm. The internet and Metamath weren't very helpful. What I came up with . . .
40K - last updated 2007-01-11 04:05 UTC by raph
Bourbaki proof checker
[[jarpiain|Juha Arpiainen]] has been working on a [[metamath]]-style proof checker in Common Lisp; it . . . detail. I'm really just getting up to speed with Metamath (and its several flavors) but as a LISP fan, . . . and I would like to advertize LISP to other Metamath heads as a potential language to work with! . . . I think it would be nice if someone in the Metamath community could write a definitive page on . . . the Metamath variants, derivatives, and associated programs . . .
7K - last updated 2006-12-20 22:19 UTC by jarpiain
Bourbaki questions
I am impressed! This is some beautiful work! And verify.lisp is amazingly short. Wow. I haven't tested . . . are null substitutions allowed? For example, in Metamath a given type could be specified as permitting . . .
4K - last updated 2005-10-22 07:49 UTC by jarpiain
Bugs
Links to pages for bugs in the current implementations of the [[Projects]] we're talking about on this . . . them to below a different project heading). '''metamath bugs''' ([[metamath|project page]]) * [[A . . . metamath bug]] * [[let and double quote]] * [[eimmimp . . .
3K - last updated 2006-12-22 09:43 UTC by fl
Collaborations
Non-[[Projects|project]]-specific collaborative efforts and jointly-written papers. =PlanetMath Documents= . . . =Presentations= ==JMM 2006 Presentations== * [[Metamathematical_Visions_-_metadata,_learning,_and_knowledge_communities]] . . .
2K - last updated 2006-01-08 16:32 UTC by jcorneli
Comments on Version 12 of the h-code page
Ray, I love the introduction, certainly couldn't have put it better myself. It is a joy to hear you discourse . . . logic-agnostic in roughly the same way that [[metamath]] is (or claims to be). rsp: "Valid s-expression" . . .
4K - last updated 2005-05-05 04:26 UTC by planetx.cc.vt.edu
Core Proof Language
(Original author: [[marnix]]) == Introduction == There is nothing new here in essence, but the new form . . . (and by extension, very similar to that of [[metamath | Metamath]]). However, it only offers a *proof* . . . In my mind, this language comes even closer than Metamath and Ghilbert to the dream of an 'assembly . . . new so far: all this is standard Ghilbert (and Metamath) stuff. As is what follows. Now for the definition . . . website can then show all proofs, just like the Metamath site does. It can show all theorems (inference . . .
22K - last updated 2006-06-27 21:06 UTC by ocat
Discussion of HDM-related things
: A number of academic projects are pursuing HDM-like goals and questions. It is not wise to ignore prior . . . MIZAR and h-code. Already a project to translate metamath into h-code is in the works. --[[rspuzio]] . . . in particular) that we find useful. Metamath is much more "our style" from a licensing . . . of view. I have no idea about the quality; but Metamath is mostly the work of one person, which could . . .
7K - last updated 2005-06-19 16:57 UTC by jcorneli
Discussion of example of structured proof
This page contains discussion about the page [[Example of structured proof]]. ---- Hmmm, I wouldn't say . . . coincidentally used the same example on the [[metamathCalculationalProofs]] page. And looking at . . . proof of this, as Marnix mentions, is [http://us.metamath.org/mpegif/xpundi.html xpundi], which uses . . . also have been used, making use of [http://us.metamath.org/mpegif/relssi.html relssi] and the fact . . . that a cross product is a relation, [http://us.metamath.org/mpegif/relxp.html relxp] (and so is a . . .
9K - last updated 2005-10-27 10:12 UTC by norm
Discussion of not really math
So what? To me, this sounds like a silly objection. For me, the relevant question here is "Is it worthwhile?". . . . it is officially classified as mathematics or metamathematics or logic or computer science or lexicography . . .
9K - last updated 2005-05-05 04:30 UTC by planetx.cc.vt.edu
Display LaTeX
I (Steve Cheng) have written a Javascript program for the Mozilla Firefox 1.5 Web browser that allows . . . first producing a grammar from an arbitrary Metamath file (so unless I called yacc as a subroutine...and . . . anyway Metamath's set.mm is said to be LALR(7), meaning lookahead . . .
24K - last updated 2006-05-14 15:34 UTC by SteveCheng
Distinctors vs binders
[[metamath|Metamath]] and friends use a metalogic based on distinct variable constraints, rather than . . . by Alfred Tarski in his 1966 paper "[http://us.metamath.org/mpegif/mmset.html#Tarski A simplified . . . system S3 on p. 11 (PDF p. 12) of my [http://us.metamath.org/downloads/finiteaxiom.pdf paper]. As you . . . as $d u ph and $d u v in set.mm. The [http://us2.metamath.org:8888/mpegif/mmset.html#pcaxioms set.mm . . . to describe the distinctor-based metalogic in Metamath. : Just a technical nit on the terminology, . . .
12K - last updated 2006-10-20 05:41 UTC by norm
Feature Requests
Links to pages describing feature requests for the [[Projects]] we're talking about on this wiki should . . . them to below a different project heading). '''metamath feature requests''' ([[metamath|project page]]) . . . * [[Logo]] * [[Metamath readline support]] * [[Open and closed intervals . . .
4K - last updated 2008-06-03 13:20 UTC by ocat
First Monday Paper--The HDM Manifesto
=Context= There are plenty of things to look at and think about on the [[HDM]] page and on the [[Discussions]] . . . been making vital contributions to the logic and metamathematics components of the project. I look forward . . . We've done some networking with PlanetMath, [[metamath]] and a few other relevant groups (which includes . . .
29K - last updated 2006-07-07 14:29 UTC by jcorneli
Focused HDM subprojects
On the way to to building the Hyperreal Dictionary of Mathematics, there are some subsets of the final . . . - Condense MMAF literature | Condense the Metamath and Friends literature]] . . .
2K - last updated 2005-10-25 19:52 UTC by jcorneli
Focussing Inward
While thinking back on PM related activities of last year, a unifying theme appears in the form of "reaching . . . gotten the attention of such organizations as Metamath, Lisp NYC, MSA, MAA and First Monday and are . . .
11K - last updated 2007-02-05 20:20 UTC by jcorneli
Formal maths bibliography
; [http://www.cs.ru.nl/~freek/qed/qed.html QED] : an apparently defunct math archiving project with some . . . that, whereas the other half is mathematics and metamathematics and Lisp and such. I figure people . . .
3K - last updated 2006-11-16 17:54 UTC by jcorneli
Free Math Award
We could have an annual award ceremony to honor outstanding contribution to mathematics. Of course, any . . . Megill for 10 years of sustained effort creating Metamath and its associated databases, set.mm and ql.mm. . . . hours tutoring students and others interested in Metamath and logic programming, but all of his Metamath . . . Bibliography sections of his webpages for the Metamath Set Explorer, Quantum Logic Explorer and Hilbert . . . 3 different programming languages!): http://us.metamath.org/mpegif/mmset.html#bib http://us.metamath.org/qlegif/mmql.html . . .
5K - last updated 2007-07-08 17:20 UTC by ocat
Free Math and Potential Bottlenecks
=On Free Math and Copyright Bottlenecks= =Proposal= Describe what is meant by the phrase "free math", . . . not?) but how some ''is'' use-friendly (e.g. the metamath stuff). The QED Manifesto would be a good . . .
9K - last updated 2005-11-13 01:19 UTC by jcorneli
General discussion of FEM
==Cash money!== The FEM has good potential for being a revenue generator for the PM site. : Does it? . . . for my [http://www.lulu.com/content/124435 Metamath book]. There are no minimums and no fees unless . . .
12K - last updated 2005-10-19 04:45 UTC by rspuzio
Ghilbert
[[image:ghilbertlogo]] Ghilbert is an extension of [[metamath]] designed for collaborative theorem-proving . . . but fix several shortcomings. Over and above metamath, Ghilbert has: * A safe definition mechanism. . . . (In metamath, definitions are conflated with axioms). * . . . Modules, with import and export. (In metamath, proofs pretty much have to be in one big . . . file). * Simple s-expression syntax. (In metamath, the grammar is user-defined, and not protected . . .
19K - last updated 2008-03-26 18:47 UTC by ocat
GhilbertVsMetamathPart1
The Ghilbert design, though somewhat sketchy, is interesting both as it relates to Metamath, and as a . . . This is only Part I. [[GhilbertVsMetamathPart2 | Part II]] is now complete, but parts . . . A lot depends on fate :) And frankly, I like Metamath. I like the idea of students and amateur, . . . making grand mistakes and learning from them. Metamath really just needs a GUI to make it more approachable. . . . trading it for a fancy new sports car? Hmmm. *Metamath vs. Ghilbert - PART I* *1. SYNTAX* Ghilbert . . .
15K - last updated 2005-09-17 18:01 UTC by ocat
GhilbertVsMetamathPart2
Back to [[GhilbertVsMetamathPart1]] The rather informal, very preliminary survey of the differences between . . . Metamath and Ghilbert continues. *Metamath vs. Ghilbert . . . to distinguish between "statements" such as the Metamath "$a" and "$p" statements and the logical statements . . . interfaces represent true statements." In Metamath there are Axiomatic Assertions and Provable . . . into the fascinating differences between the Metamath and Ghilbert Proof Verification Engines!!! . . .
23K - last updated 2006-11-20 23:19 UTC by ocat
Ghilbert Pax
An important part of the greater [[Ghilbert]] project is Ghilbert Pax: the "portable axiomatization." . . . of the predicate calculus, unlike that of Metamath, is typed. This should help when porting pax . . . The axiomatization is taken directly from Metamath. == pred == The axiomatization of predicate . . . calculus with equality roughly follows Metamath's, but with some significant differences. . . . (not free in) operator, defined similarly to Metamath's "ph -> A. x ph", but with biconditional . . .
7K - last updated 2007-01-20 23:08 UTC by Bob Solovay
Ghilbert and HDM
: ''I would be happy to cooperate with The Hyperreal Dictionary of Mathematics project if they choose . . . things, besides proof verification. For example, metamath has "meta" information about typesetting in . . . quaternions. Note the similarity to [http://us.metamath.org/mpegif/mulcom.html mulcom] in Metamath's . . . outside the domain of the function ([http://us.metamath.org/mpegif/ndmfv.html ndmfv]) Thus, in the . . . itself, which is trivially provable ([http://us.metamath.org/mpegif/eqid.html eqid]). An axiomatic . . .
33K - last updated 2006-11-29 19:52 UTC by marnix
Ghilbert automation
One of the main reasons I've been so insistent that [[Ghilbert]] be simple is so that some of the more . . . seen, converting a resolution-based proof into Metamath steps is not trivial, and doing so simplistically . . . meta-question of "is X provable in a sequence of metamath steps", but in direct translation. * [[Mathematical . . . are fairly large. Bob Solovay reimplemented my Metamath proof of [http://us.metamath.org/mpegif/nn0opth.html . . . steps", as opposed to the exacting detail of Metamath proofs. For two, MV, seems to emphasize implication . . .
13K - last updated 2006-11-29 19:51 UTC by marnix
Ghilbert fast and dumb
One of the things I've been musing over is the nature of the "fast and dumb" theorem prover for [[Ghilbert]]. . . . hypotheses" could perhaps be elided. As in the Metamath Solitaire applet, it's possible to omit them . . .
8K - last updated 2006-11-29 19:50 UTC by marnix
Ghilbert is not AI-complete
Very briefly put, [[Ghilbert]] is not AI-complete, but it is AI-friendly. The success of the broader . . . QED Manifesto]. I find it impressive that the Metamath set.mm database was developed with essentially . . .
3K - last updated 2006-11-29 19:51 UTC by marnix
Ghilbert specification
'''Important:''' This specification is not complete. As of 20 Oct 2006 major work is underway. The language . . . assigning kinds to variables (analogous to $f in Metamath). * "term" commands introducing new terms. . . . each constraint corresponds to a $d command in Metamath). The hypotheses are a list, with each hypothesis . . . each hypothesis corresponds to a $e command in Metamath). The consequent is a valid term. It corresponds . . . latter without the corresponding $= clause) in Metamath. == Proof files == === import === An "import" . . .
15K - last updated 2006-10-20 15:07 UTC by jorend
Ghilbert specification discussion
(See [[Ghilbert specification]].) == Declarative vs. procedural == Metamath is specified declaratively . . . declaratively. -- [[raph]] :: . :: Well, the Metamath spec is mostly declarative and reads very . . . here...) The main thing I focused on in the Metamath spec, more than declarative vs. procedural . . . self-contained so that no knowledge of Metamath, proofs, logic, or programming was prerequisite. . . . correct, without ever checking it with the metamath program. (I checked it after he declared it . . .
18K - last updated 2008-03-31 14:18 UTC by GrafZahl
Ghilbert syntax plans
: *Update 2 Sep 2006:* I'm prototyping a conversion from Ghilbert s-expressions to reasonable math typesetting, . . . fonts is of course very heavily influenced by Metamath's, both the GIF and !LaTeX outputs. I'm short . . . ASCII notation, very similar to what Metamath does now, but with fewer parentheses and much . . . ASCII notation, very similar to what Metamath does now, but with fewer parentheses and much . . . Whitespace was optional in the original Metamath language/program, and the algorithm was as . . .
30K - last updated 2006-09-05 15:38 UTC by 65.91.2.68
HDM Feasibility Study discussion
I think that a proper Feasibility Study could secure funding and personnel for subsequent phases (Requirements . . . experiment will settle the matter. You and other metamath folks are right to be highly skeptical of . . . who will want to do what with it. P.S. Why is Metamath so excellent, so intriguing? It is supported . . . it is elegant, true. But it is "scientific". The Metamath.pdf specifies precisely how to recreate the . . . results of metamath.exe. Anyone who wants can repeat the experiment, . . .
23K - last updated 2005-10-31 17:12 UTC by jcorneli
HDM SOC proposal
=describe your idea/project in 10 words= building a lisp-based mathematical language that anyone can . . . language design. * Learn about mathematics and metamathematics. * Learn about and practice parsing, . . .
3K - last updated 2005-06-05 00:57 UTC by jcorneli
HDM and logic agnosticism
This topic seems to be undergoing discussion in several places. At the risk of being repetitive, let . . . point. The issue is not simply one of logic or metamathematics, but also of linguistics and AI. We . . . because we find just about everything from metamathematics to applied mathematics embedded in . . .
2K - last updated 2005-09-21 05:59 UTC by ocat
HDM criticism
Since I learned that Google would not sponsor any of the HDM projects, I have not been very active here . . . plan, be verifiable using a system based on the metamath proof checker. The parser mentioned above . . .
45K - last updated 2005-07-21 20:04 UTC by jcorneli
HDM practitioner work habits
A simple, flippant answer to your question about me going full-time might be "a full-time salary of $30 . . . be regarded as the transposition of Goedel's metamathematical theme to the key of Planet Technae . . .
13K - last updated 2005-10-27 08:43 UTC by rspuzio
HDM release timeline
''By the time we have the [[scholium system]] working and the APM-Xi (HDM-p2) content is ported to [[hcode]], . . . corresponding implementation of a "friend of [[Metamath]]". These abstract ideas are all fine and . . .
3K - last updated 2006-12-06 21:35 UTC by jcorneli
HilbertizedNatDed
(back to [[mmj2]] ) NOTE: this .mm file does not simplify things. It does not seem like a good idea... . . . really need is a textbook designed for use with Metamath. --[[ocat]] 25-Sep-2006 Revised *proposed* . . . you have in mind for the mechanics of how Metamath proofs work, there is a feature you may or . . . may not be aware of in the metamath program: MM> show proof equid /detail 32 . . . out the substitutions in e.g. [http://us2.metamath.org:8888/mpegif/biigb.html biigb]. :) By the . . .
9K - last updated 2006-09-26 02:57 UTC by ocat
HomePage
= FYI: Obtaining permission to edit = This wiki is access-restricted, due to persistent spamming that . . . AM is also, fittingly, the wiki home of the [[metamath]] family of projects. You'll find discussion . . .
3K - last updated 2008-04-22 16:46 UTC by jcorneli
How to Check Proofs
This page is meant to give a description of the technique I plan to implement for checking proofs for . . . so one could use any other formal system (metamath, mizar, etc.) just as well. ** Justifications . . . a consistent set of substitutions over all. In Metamath there is a theorem with 19 hypotheses, so . . .
11K - last updated 2006-06-15 18:18 UTC by marnix
Introduction to Connections as Functors
A fundemental concept in differential geometry is the connection. Basically, a connection on a space . . . in particular, I hope it will be of use in metamathematics to describe how mathematical notions . . .
1K - last updated 2005-05-05 04:38 UTC by planetx.cc.vt.edu
Introduction to What is a Mathematical Entity
In mathematics, one studies such entities as numbers and geometrical figures. To discourse about these . . . of axiomatization. The purpose of this essay in metamathematics is to explore how the same mathematical . . . as our inspiration and try to develop metamathematical analogies of these geometric constructs. . . .
3K - last updated 2006-10-30 05:06 UTC by raph
JACKYL
We've done a few proofs already... they aren't that formal, and for many more, more formal proofs, see . . . [[metamath]]. But the proofs we've done might be worth . . .
7K - last updated 2005-06-18 18:24 UTC by jcorneli
JHilbert
JHilbert is a proof verifier for collaborative theorem proving in the spirit of [[Ghilbert]]. Visit the . . . Of course, you don't /strictly/ need them. In metamath, definitions are just axioms with equivalence . . . custom-made for feeding data from/to Metamath and other systems such as jhilbert: the "mmj2 . . . mode. The Book Manager imposes an ordering on a Metamath database, breaking it down into chapters and . . . which may be helpful. The interface /to/ Metamath may be harder because the names must be converted . . .
14K - last updated 2008-09-15 09:23 UTC by GrafZahl
JHilbertDiscussion
=implementation independent specifications= I wonder if, for example, it is an error -- in the long run . . . It appears that JHilbert is using RPN style (Metamath) proofs. This is a good way, but it is also . . . has the benefit of clarity (as compared to the Metamath proof verification algorithm with is non-obvious.) . . . instead of an array (long list) of labels. Metamath proofs, and (JHilbert as written) have a macro . . . I've always seen the forward-chaining nature of metamath as an advantage over other systems if you . . .
41K - last updated 2008-09-19 21:29 UTC by GrafZahl
Joseph A. Corneli
Joseph A. Corneli was born in Steven's Point, Wisconsin, in 1979, and received the degree of Bachelor . . . this period, he read works in philosophy and metamathematics, attended several classes in the computer . . .
3K - last updated 2007-01-16 15:36 UTC by jcorneli
July 12 LispNYC Talk
=Announcement= Please join us for our next meeting on Tuesday, July 12th from 7:00 to 9:00 at Trinity . . . This talk will be of interest to mathematicians, metamathematicians, and lispers, and especially interesting . . . appreciation of the subtle beauties of logic and metamathematics. This program led him to enroll as . . .
7K - last updated 2005-12-11 00:39 UTC by jcorneli
LISP
LISP uses lots of parentheses and makes life incredibly easy for the programmer. Everything between paretheses . . . Programs by G. J. Chaitin] --- In addition to metamathematics, this article provides a nice introduction . . .
4K - last updated 2005-05-05 04:38 UTC by planetx.cc.vt.edu
Lambda calculus based metamath system
Some notes about a future lambda calculus based metamath system. #1: First the constants $c L $. is for . . . It seems appropriate to be used with metamath. It is very similar to the previous one. Except . . . the fact that variables are not independant in metamath is important. "The Lambda Calculus is then . . .
3K - last updated 2006-04-04 12:40 UTC by frl
Let G be a group
Please see the discussion section on [[list of formal statements in natural language]] for an overview . . . functions described there. Still to go, "metamathematical" (maybe) and "set-theoretical". (Note . . .
6K - last updated 2005-05-05 04:39 UTC by planetx.cc.vt.edu
Linguistic analysis of mathematics, by Arthur F. Bentley.
=Citation= Bentley, Arthur Fisher, 1870-1957. Linguistic analysis of mathematics, by Arthur F. Bentley. . . . the ideas from the book. The style was somewhat metamathematical, but also somewhat "metaphysical". . . .
4K - last updated 2005-05-05 04:39 UTC by planetx.cc.vt.edu
LispNYC Jan 10 talking points
These are the talking points I dealt with in [[January 10 LispNYC Talk|my LispNYC talk]]. The only one . . . * Mathematics is mostly formal and contains metamathematics. * Computers are designed for things . . .
2K - last updated 2006-01-17 17:48 UTC by jcorneli
Logo
I wonder if we could have a Metamath Logo a bit less -- let's say -- californian. Something in a circle . . . 2004 email: > Someday I should revisit the Metamath's aleph - it was done in the early > 90s . . .
2K - last updated 2008-06-04 14:28 UTC by ocat
MMHDM1 deliverables
Phase 1 HDM Deliverables: * Language Specification * Standard Math Symbol/Object Ontology for HDM * Parsers/Reverse . . . library of definitions, theorems, proofs, and metamathematics". I don't think a GUI is particularly . . .
2K - last updated 2005-09-23 02:06 UTC by ocat
MMHDM1 ghilbert compatibility
There are substantial advantages to making HDM file-compatible with Ghilbert: 1. Norm and Raph have already . . . of mathematical knowledge already encoded in Metamath including Propositional Logic, Predicate Logic, . . . collections of (meta)mathematical content, and Metamath's library is an essentially perfect candidate . . .
9K - last updated 2005-09-24 01:06 UTC by jcorneli
MMHDM1 hcode
To get HDM up and running, the key task is linguistic. It's all about "H-Code", or whatever common object . . . comprise the primary incompatibility between Metamath/Ghilbert and H-Code, IMO.) Second, it should . . .
6K - last updated 2005-09-23 21:56 UTC by jcorneli
MathML
Why does !MathML suck so hard? [http://www.dataweb.nl/~cool/Papers/MathML/OnMathML.html The Disappointment . . . to write open source software for something like Metamath/Ghilbert without getting into patent land...all . . . in several fonts side by side here: [http://us2.metamath.org:8888/fontcompare.gif fontcompare.gif] . . . look as good as the !LaTeX font or even the Metamath bitmaps. The character sizes and shapes seem . . . you need. It would be possible to create a Metamath Font and specify that in your webpages, but . . .
10K - last updated 2006-09-07 13:09 UTC by norm
Mathematical Counter-cultural Appeal
=PlanetMath rocks!= That's what I heard (literally) from several people at the Joint Mathematics Meeting . . . which to pursue my intellectual ruminations on metamathetics(which easily extend to all sorts of subjects) . . .
41K - last updated 2006-02-21 04:10 UTC by rspuzio
Mathematical Provers, Proof Assistants, and Formal Math particularly relevant to HDM
Please revise entries to show relationships to [[HDM]]. --[[jcorneli]] Mon Jun 20 04:48:37 2005 UTC This . . . : lisp-based automatic theorem proving. ; [[metamath]] : Metamath is a tiny language that can express . . . Ghilbert ] : (derivative work of metamath; unlicensed) ; [http://www.calculemus.net . . .
6K - last updated 2006-03-19 20:26 UTC by jcorneli
Mathematical Vernacular
The term "mathematical vernacular" ("wiskundige omgangstaal" in the original Dutch) was introduced by . . . MV proofs into explicit proofs verifiable by [[metamath]] and friends must contain a first-order prover . . . xxx is provable." (Search for "twist" on [[metamathMathQuestions]] for a description.) It worked . . . relatively straightforward to translate into a metamath-like langauge. For one, [[frl]] has proposed . . . an axiomatization of [[Natural_deduction_based_metamath_system|natural deduction]] in metamath. Also, . . .
10K - last updated 2007-03-27 21:10 UTC by fl
Mathematical logic particularly relevant to HDM
=Fun stuff= ; http://en.wikipedia.org/wiki/Existential_graph : This seems like a reasonable place to . . . set theory. I have worked out the details for [[metamath]], which are described in a [[http://us2.metamath.org:8888/downloads/megillaward2005he.pdf . . . of the technique.--[[norm]] 20-Nov-05 =Metamathematics= ; ''A Theory of Sets'' by A. P. Morse . . . Boyer). It would be interesting to compare to [[metamath]]. : [[norm]]: I would like very much to hear . . . of a Morse set theory verifier with the Metamath-type verifiers. Or to determine whether Morse . . .
6K - last updated 2006-12-19 21:12 UTC by jcorneli
MaximallyCompressedMetamathDatabases
Here is a first draft of "compressed1.mm" which documents how a Metamath database can be "maximally" . . . Metamath source file for experimentation with Maximally . . . Compressed Metamath databases. #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# . . . are required by law. ===== Maximally Compressed Metamath Databases. ===== The idea behind "maximally" . . . compressed Metamath databases is that a theorem's formula and . . .
6K - last updated 2008-05-10 21:53 UTC by ocat
Metamath
#REDIRECT [[metamath]] . . .
1K - last updated 2006-12-06 21:36 UTC by jcorneli
MetamathForProgrammers
I have been thinking about writing a small "book" (html w/.jpg diagrams) titled something like, "Metamath . . . be similar in both intent and implementation to "Metamath For Dummies". One reason this is a good idea . . . speak, "language agnostic" (this builds upon the Metamath system which has only these built-in inference . . . all that. It should be possible to begin with Metamath and let interested students delve into its . . . the generation process.))) I can also equate the Metamath Proof Verification Algorithm directly to the . . .
7K - last updated 2008-04-22 18:26 UTC by ocat
MetamathOMDocBridge
[mmj2 mmj2] [http://www.mathweb.org/wiki/Metamath_to_OMDoc_Bridge . . . page] [MetamathOMDocBridge20070304 Archive-Prev As Of 2007-03-04] . . . by actually performing the implementation of MetaMathOMDoc Bridge are insufficiently different from . . .
4K - last updated 2007-03-24 14:21 UTC by ocat
MetamathOMDocBridge20070304
[MetamathOMDocBridge current page] I am interested in working out the specifications for converting between . . . OMDoc and Metamath ".mm" files At this time that means set.mm . . . software provides a way to obtain a fully parsed Metamath database in RAM, which can easily be output . . . such as unification and import/export via Metamath's eimm.exe utility. Ideally a collaborator . . . I want to do is advance the state of the art of Metamath, mmj2 (my project), and OMDoc, while benefiting . . .
33K - last updated 2007-03-05 17:03 UTC by ocat
Metamath readline support
== Feature request: Metamath readline support == If you've used the precompiled version of the [[metamath]] . . . [http://us2.metamath.org:8888/index.html#mmprog program] on Windows, . . . this kind of behavior. Interfacing readline to Metamath that would be a very useful project. If anyone . . . is interested, here are some details about the Metamath program that may prove helpful. Almost all . . . user input in metamath is funnelled through one line in mminou.c: . . .
6K - last updated 2005-11-26 19:15 UTC by norm
Metamathematical Visions - metadata, learning, and knowledge communities
20 minutes to say what metadata, learning, and knowledge communities are about. HDM. Scholium System. . . . arises from multiple subjectivity) # traditional metamathematics: "linguistics of mathematics". neo-metamathematics: . . . a lot of other people will have heard of other metamathematical projects already (and I don't mean . . . either of what you've put under "traditional metamathematics"). Perhaps a section where you relate . . .
4K - last updated 2006-02-21 23:37 UTC by jcorneli
NSF Cyberinf 2007 Grant Draft 1 Discussion
This is a page discussing [[NSF Cyberinf 2007 Grant Draft 1]]. ---- A first comment. One of the major . . . have observed this requirement as it relates to Metamath. mmj2 was written partly, as a first step, . . . for us, it comes down to "there is some Metamathematical System, A, and it is not immediately . . . clear if this system is compatible with Metamathematical System B, so there are two disjoint . . . time being, largely separate evolution." And the Metamathematical Systems might seem superficially "ametamathematical"; . . .
17K - last updated 2006-12-27 22:24 UTC by jcorneli
NatMmInMmj2
$( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#* Metamath source file . . . # has no particular meaning. It is mandatory in metamath to begin formula with a constant and it is . . . by Pfenning is not rich enough to work with in metamath. En effet ??? it presupposes substitution . . . level (i. e. by an independant device). In metamath such a device doesn't exist. Thus we must . . . is managed at a metalogical level. Since in metamath we can't do that I added axioms. 3 -- I added . . .
94K - last updated 2006-02-11 14:11 UTC by ocat
Natural deduction based metamath system
$( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#* Introduction Metamath . . . I recommend the reading of ` Introduction to metamathematics ` by Kleene chapter V (In fact I'm . . . ` has no particular meaning. It is mandatory in metamath to begin formula with a constant and it is . . . by Pfenning is not rich enough to work with in metamath. En effet ??? it presupposes substitutions . . . level (i. e. by an independant device). In metamath such a device doesn't exist. Thus we must . . .
103K - last updated 2006-12-06 17:16 UTC by jorend
Notes on Various Proof Systems
This page was started by [[raph]] in response to some discussion about Mizar in comparison to [[metamath]]. . . . major theorem provers out there. =Provers= == Metamath / Ghilbert == Metamath, and its offshoot Ghilbert, . . . There's already a lot of discussion on the [[metamath]] page, which maybe should get refactored . . . be so converted is tricky in a large library. Metamath contains the axiom of choice but not (directly) . . . Megill has also done followup work on [http://us.metamath.org/downloads/megillaward2005he.pdf Emulating . . .
16K - last updated 2006-08-19 03:28 UTC by raph
OMDocSchemaQuestions
return to [[MetamathOMDocBridge]] ==2007-03-22: More possible questions and such about the OMDoc 1.2 . . . and calls them abstract data types. What the Metamath -> OMDoc Bridge project needs to be able . . . content. Furthermore, the charm and elegance of Metamath lies partly in the fact that a Metamath database . . . in the PDF file itself like in [http://us.metamath.org/downloads/metamath.pdf metamath.pdf], . . . can also be used, as is done in [http://us.metamath.org/latex/metamath.tex metamath.tex]. However, . . .
23K - last updated 2007-03-22 19:22 UTC by ocat
Old Events
Things that have already happened. =2007= ==January== * (Over) NSF Cyberinfrastructure Grant proposal. . . . are: * [[PlanetMath and Free Mathematics]] * [[Metamathematical Visions - metadata, learning, and . . .
6K - last updated 2008-05-06 23:29 UTC by jcorneli
Open and closed intervals in R
Hi Norm, we have recently spoken by mail of open and closed intervals in RR. I have just come across . . . for the existing ZZ intervals [http://us.metamath.org/mpegif/df-uz.html df-uz] and [http://us.metamath.org/mpegif/df-fz.html . . . complain that the former is confusing in the Metamath program or mmj2, then ( A (,] B ) is my second . . .
8K - last updated 2006-12-26 22:09 UTC by norm
PlanetMath and Free Mathematics
20 minutes to say what "free math" and PM.org are all about and why they are important. = Goal of the . . . be thinking about what to do/say/show for the [[Metamathematical Visions - metadata, learning, and . . .
7K - last updated 2006-01-12 14:40 UTC by jcorneli
PlanetMath as E-Institute
Although I mentioned HDM research in this category (which is exactly where I think it belongs), I didn't . . . areas, as well as fairly strong connections to metamathematics, social theory of collaboration, philosophy . . .
12K - last updated 2006-03-13 02:51 UTC by rspuzio
PlanetMath whitepaper disposable comments
Hello Aaron, I read your comments concerning the "whitepaper" and I applaud you. Outstanding!!! There . . . helpful; we do not need a professor to check a Metamath proof for correctness -- we have the Proof . . .
10K - last updated 2006-02-14 00:01 UTC by jcorneli
Plans
This page complements the [[Schedule]]. While the schedule is concrete, our plans are still somewhat . . . and proof-checker that will work with the [[metamath]] content. Another goal is to convert HDM-p3 . . .
7K - last updated 2005-05-14 19:39 UTC by jcorneli
Plans formulated after NSF CIO 2007 grant submission
=Planning for 2007 (and, where possible, beyond)= These plans relate at least to PlanetMath and HDM for . . . rest of the MathWeb and similar "socio-technical metamathematics" groups * our individual contacts (see . . . Miller, Kohlhase, many others (including our metamath neighbors and folks in various localities). . . . to improve collaborration between HDM and metamath and further the dialogue which began last . . .
35K - last updated 2007-05-10 05:09 UTC by akrowne
Plasma OCR
I'm planning an OCR program. Would you like to mentor such a project? --[[alih]] Maybe! AFAIK, there . . . the mathematical logic community. I'm sure the metamath people would find it useful, especially since . . .
27K - last updated 2006-06-09 20:12 UTC by jcorneli
PrecomputationOfLogHypUnifiers
I have been considering opportunities for parallel processing during the proof search process. Several . . . answers remain valid for the originally input Metamath database except in the case of new theorems, . . .
13K - last updated 2008-11-07 12:28 UTC by ocat
Principal instances of metatheorems
In [[U2ProofVerificationEngine]], I described how a single metatheorem in Metamath/Ghilbert may translate . . . this simple theorem, an instance of [http://us.metamath.org/mpegif/ax-4.html ax-4] followed by two . . . applications of [http://us.metamath.org/mpegif/ax-gen.html ax-gen]: A. x A. y . . . my [[Ghilbert Pax]] version of [http://us.metamath.org/mpegif/hbal.html hbal] (called nfi_al . . . that the Ghilbert Pax versions of [http://us.metamath.org/mpegif/alcom.html alcom] and [http://us.metamath.org/mpegif/aaan.html . . .
20K - last updated 2006-12-13 16:45 UTC by norm
Projects
Major projects related to commons-based peer production of free content that come to mind; please add . . . Dictionary of Mathematics]] * [[MathWeb]] * [[metamath]] (and friends) ** [[mmj2]] ** [[bourbaki]] . . . ** [[IsarMathLib]] ** [[Natural_deduction_based_metamath_system]] ** [[Lambda_calculus_based_metamath_system]] . . .
3K - last updated 2008-04-15 21:21 UTC by jcorneli
Puzzling behavior when adding a Feature Request
The following happened when I tried to add a feature request by editing the [?action=browse;anchor=0;id=metamath_feature_requests . . . metamath_feature_requests] page, linked to from the . . . page in the comment "[the page metamath_feature_requests also exists]". After I edited . . . metamath_feature_requests] . . . metamath_feature_requests]. . . .
3K - last updated 2005-12-01 18:21 UTC by norm
Real numbers on PM
'''Aim''': This aim of this project is to chart, proofread, and improve the topic of real numbers on . . . there is an alternative proof at http://us.metamath.org/mpegif/mmcomplex.html . It is slightly . . . where theorems or even proofs on PM have their Metamath formalizations done already. Having links . . .
13K - last updated 2007-04-26 21:31 UTC by Wkbj79
Relationship between Free Math and Free Software
There are lots of free software packages that have to do with mathematical science, cryptography, or . . . sort of thing can useful: I hadn't heard of [[metamath]] until someone brought it up on the PM forums. . . .
3K - last updated 2005-05-05 04:53 UTC by planetx.cc.vt.edu
RunParmsForNatMmInMmj2
===== * sample for frl, 11-Feb-2006. * note: RunParms have much * documentation in c:\mmj2\src\mmj\util\UtilContants.java . . . LoadFile,c:\metamath\frl\expFRL20060130.mm VerifyProof,* Parse,* . . . ProofAsstProofFolder,c:\metamath\frl\myproofs RunProofAsstGUI . . .
1K - last updated 2006-02-11 14:29 UTC by ocat
Shaneal
=A Flexible LISP Proof Checker= By: Shaneal Manek (smanek@gmail.com) ==Introduction== Mathematics is . . . direction that might be considered is a Metamath to h-code converter that would allow PlanetMath . . . to augment their existing theorem libraries with Metamath’s. All of these are just ideas for where . . . the end of this Summer of Code. : Rather than [[metamath]] to h-code, a more natural fit for a LISP-based . . . whose syntax is based on S-expressions. A Metamath to Ghilbert translator already exists. --[[norm]] . . .
19K - last updated 2006-05-11 15:46 UTC by 82.lib.elmhurst.edu
Small Projects - Condense MMAF literature
Now that [[metamath]] creator/users have joined onto this site, we have a good chance to ask them questions. . . . it would be handy for the HDM project to have a metamath and friends (MMAF) quick-start guide. Since . . .
1K - last updated 2005-10-25 19:54 UTC by jcorneli
Small Projects - Literature review
The page [[HDM-related things to check out]] has a number of leads, but they are quite disorganized. . . . worth checking out at this point are [[metamath]] and probably (for a point of comparison) . . .
1K - last updated 2005-10-25 19:57 UTC by jcorneli
Small Projects - Sort and standardize HDM-p3
There are already 100 definitions in something similar to hcode written down in HDM-p3. Someone could . . . warm-up for other porting projects (e.g. porting metamath or p2/APM-xi). --[[jcorneli]] . . .
1K - last updated 2005-07-13 11:58 UTC by jcorneli
Small Projects - Version Zero
As a proof of concept, one could consider a miniature version of HDM which is restricted to propositional . . . logic. This can be obtained by processing the metamath database through the parser. ---- [[Focused . . .
1K - last updated 2005-06-27 03:12 UTC by jcorneli
Tasks
Links to pages for tasks related to the [[Projects]] we're talking about on this wiki should be posted . . . will move it for you at an appropriate time). '''metamath tasks''' ([[metamath|project page]]) '''Noösphere . . . proofs of various interesting facts]] * [[port metamath to something our ai will like]] * [[write . . .
4K - last updated 2006-03-03 02:13 UTC by akrowne
The Hyperreal Dictionary of Mathematics
=What is the Hyperreal Dictionary of Mathematics?= You could read a whole essay about that question, . . . [[From me to you - Still more HDM planning]] * [[metamathAndHdmPhaseI|Plans involving HDM together with . . . Metamath]] * [[JACKYL|JACKYL - a foray into proving . . .
4K - last updated 2007-04-30 19:21 UTC by jcorneli
The important components of the HDM project
At present there are four main areas of the project; some can be found in [[HDM CVS]], but please take . . . flexible system for doing formal proofs. (The [[metamath]] project provides a free system that we may . . .
2K - last updated 2006-11-07 00:57 UTC by jcorneli
Theorem database
So, an idea I had lying around in my head for some time. It seems vaguely related to PlanetMath, though . . . to you. -- [[alozano]] Also look at [[metamath]]. --[[jcorneli]] . . .
2K - last updated 2005-05-05 04:56 UTC by planetx.cc.vt.edu
Timetable for PlanetMath development
A journey of a thousand miles begins with a single step. --The Tao, Chapter 64 During the last year, . . . (machine verified) mathematics or not. Metamath is discussed on this wiki, so that would indicate . . .
14K - last updated 2006-03-02 12:02 UTC by jcorneli
Tips for using AsteroidMeta
First of all, read the [[Policy]]! That will make the simple things work well. Once you've mastered the . . . indented paragraphs? == At the bottom of the [[metamathMathQuestions]] page, I added a long quotation . . .
5K - last updated 2008-03-26 16:48 UTC by akrowne
Translation Systems
On the [[Notes on Various Proof Systems]] page, [[jcorneli]] asked about the state of the art in translations . . . is far from encyclopedic. --[[raph]] == Metamath to Isabelle/ZF == I am working on importing . . . Metamath theorems into Isabelle/ZF. The latest (1.2.0) . . . 500 proofs I have encountered an issue with how Metamath and Isabelle/ZF treat the intersection of . . . set is treated as not defined). This means that Metamath's [http://us.metamath.org/mpegif/elint.html . . .
21K - last updated 2007-03-27 17:18 UTC by ocat
Two years later
This is meant as a successor to [[Half a Year Later]]. Like its predecessor, it is a progress report . . . characterization of Goedel's work as coordinate metamathematics apt, in the same vein viewed my theorem . . . of recursive functions as differential metamathematics, and where coordinates and diferential . . . of new possibilities opened up by coordinate metamathematics rather than get hung up over an impossibility . . . too connectons provide an example, but in a metamathematical fashion. In the coordinate formulation . . .
147K - last updated 2007-01-14 18:57 UTC by norm
U2ProofVerificationEngine
*Requirements for an Alternate Version ("U2") of the Metamath Proof Verification Engine using Traditional . . . Variable Concepts* ----- =The Problem= Metamath's use of "Distinct Variable Restrictions" . . . have previously limited usage and acceptance of Metamath because: * Students, particularly "self-learners", . . . when translating textbook formulations to Metamath. (And isn't it easier to clone part of Metamath . . . ago hardwired in their brains. Combined with Metamath's lack of a First order Prover, the use of . . .
73K - last updated 2006-12-12 02:44 UTC by ocat
UsingMolecularMemoryTech
[http://www.computerworld.com/action/article.do?command=viewArticleBasic&articleId=9045078 Nanotech . . . our project ambitions. For example, consider Metamath databases, like set.mm which are intended . . . that the particulars of the concrete syntax (Metamath's ASCII shorthand) are somewhat arbitrary, . . . that there are at most 999 variables in a single Metamath formula. And we assign the variables in a . . . with proof step formulas instead of being in Metamath RPN format, we would be able to easily search . . .
7K - last updated 2007-11-02 15:53 UTC by ocat
Version Zero
This page will discuss the specification and implementation of the zeroth version of h-code. In the interests . . . [[grammar for hcode]] ==Inbuilt Functions== ===Metamathematical=== defthm ; defn : * '''Usage''': . . .
5K - last updated 2005-07-08 17:39 UTC by jcorneli
What is Free Culture
Intuitively, I like the merge "free content" + "culture" -> "free culture" on the [[Discussions]] . . . from trekking the crystalline slopes of Mt. Metamath, try a *free* book about being free...in some . . .
23K - last updated 2005-11-16 04:25 UTC by jcorneli
What is a Mathematical Entity
Although this essay may at first sight appear to be "pie in the sky" abstract speculation involving category . . . the whole story. What I had in mind was more metamathematical than that. With the right perspective, . . .
8K - last updated 2006-10-31 02:35 UTC by rspuzio
What is a Mathematical Entity - Categories and connections
In differential geometry, one encounters situations in which an entity such as a vector or a tensor is . . . to another. An analagous situation happens in metamathematics --- one might start with a particular . . . differentiability will not play a role in our metamathematical applications, we shall not concern . . .
3K - last updated 2005-05-05 04:57 UTC by planetx.cc.vt.edu
WhyAreMetamathProofsSoShort
= Why are Metamath proofs so short? = Metamath's set.mm database encodes a rich slice of mathematical . . . the mandatory hypotheses is reasonable; some Metamath variants, including Norm's "solitaire" java . . . the proofs so short? Especially in comparison of Metamath's design to that of other proof systems, the . . . answer is far from clear. Metamath forces proofs to be explicit and detailed . . . base case and the induction step by itself. Yet, Metamath, with no such sophistication, manages proof . . .
11K - last updated 2005-12-21 17:53 UTC by norm
Why I am frustrated by the idea of writing an HDM Manifesto
I think that a manifesto (at least, these days) is supposed to be a document that stands behind a social . . . crew. No messing around. We code, learn enough metamathematics & linguistics, etc., to at least . . .
8K - last updated 2006-07-07 16:19 UTC by jcorneli
antecedents
When I develop a proof I rarely have the courage to abandon an antecedent in the list of antecedents . . . which removes the antecedents for me (either in metamath or in mmj2) or a way to highlight the never . . . France is :-) --[[ocat]] ===Workaround for the metamath program=== Unfortunately, there is currently . . . of "proof repair" could be useful. For the metamath program, there is a script that I often use . . .
8K - last updated 2008-05-19 17:43 UTC by ocat
beyond harry potter
RMS is [http://www.stallman.org/harry-potter.html suggesting] that people not buy harry potter books. . . . If this book is relevant to research on Metamath then I don't see any reason not to cite it . . .
11K - last updated 2005-11-16 05:08 UTC by ocat
bootstrap problem for hdm parser
(Conversational: I am wondering about hooking up/expanding this: [[grammar_for_hcode]] with this: [[What_can_the_expression_parser_do]]. . . . [[designing_proof_structures_for_hcode]] -- the Metamath/Ghilbert proofs construct formulas by supplying . . . axiom or definition which can be checked. Metamath.pdf has stuff about "condensed detachment" . . . a programming language, but as a mathematical or metamathematical framework. This is not too wild given . . . 1. I suggest having a look at the Ghilbert/Metamath comparison, parts 1 and 2 (so far): [[GhilbertVsMetamathPart1]]. . . .
16K - last updated 2005-10-26 16:50 UTC by jcorneli
dan
Getz Dan - Metamath and friends (ghilbert...) reader (for the time being). Email: lastname firstname . . .
1K - last updated 2006-11-22 12:04 UTC by dan
designing proof structures for hcode
This is a page can be the place to talk about issues in hcode design that are specifically related to . . . in propositional calculus as expressed on Metamath: http://de.metamath.org/mpegif/id1.html I'm . . .
3K - last updated 2005-06-25 00:51 UTC by jcorneli
discussion of quote
Even though I said I wouldn't say more on this topic of quotes, allow me to change my mind some and at . . . role in hcode. Yes we definitely want it at the metamathematical level. And maybe we do want it to . . .
7K - last updated 2005-05-05 05:03 UTC by planetx.cc.vt.edu
distributivity of intersection over union
This proof is based on the proof given in Autexier and Fiedler, "Textbook Proofs Meet Formal Logic -- . . . rule is being applied to, it is somewhat more metamathematical than "antecedent and inference rule", . . .
3K - last updated 2005-07-11 15:43 UTC by jcorneli
fair use of code snippets
The code for "the metamath book" includes a few lines that define a latex package, but which weren't . . .
7K - last updated 2006-07-24 16:35 UTC by norm
finding new content for PM
Gutenberg-US has some math books. These should all be public domain in the US. However, they do not seem . . . instead of being deleted in 2003. --[[matte]] * metamath.org - contains more than 8,500 theorems and . . . if PM provides the file layout specs. Metamath is a very remarkable achievement. Starting . . . learn more about the past, present and future of Metamath! --[[ocat]] 5-Mar-2006 ==== Discussion ==== . . . with translation mechanisms between them. E.g. a metamath entry that corresponded to a given "standard" . . .
29K - last updated 2006-05-08 23:58 UTC by bloftin
fl
== Yes, sir == "A computer program is a piece of literature." Knuth ([http://tex.loria.fr/typographie/mathwriting.pdf . . . mécanique. Des entreprises telles que le projet metamath[55] ou le projet Ghilbert,[56] peuvent donner . . . rules of a mechanical syntax. Projects such as Metamath or Ghilbert can give an idea of such a research . . . agree, but playing with it in the context of Metamath has led me to appreciate how powerful a hack . . .
8K - last updated 2008-10-02 21:43 UTC by ocat
fl's sandbox
This page is a temporary holding place for [[metamath]] code to be communicated to [[norm]], when it . . .
1K - last updated 2008-02-18 13:07 UTC by ocat
hdm's formal system
For now, you should see [[metamath]]. We will probably re-implement the metamath proof checker and metamath . . . or go ahead and chime in. = Proof checking = The metamath project has checked lots of proofs - we can . . . when relevant. [[Levels of Proof Checking]] [[Metamathematics and Quotation]] = Translation hcode . . . it so we can treat various different branches of metamathematics within one system. = Expressing formal . . . fiction movie. But actually, this is what metamathematics is about. If we provide one metamathematical . . .
4K - last updated 2006-06-27 20:31 UTC by rspuzio
hdm's parsing system
We have a simple parser for math expressions -- really, in development, but it certainly works on some . . . UTC We might also consider drafting off of [[metamathGrammarFacilities]] and then generalizing. . . .
3K - last updated 2006-11-30 17:50 UTC by jcorneli
igblan
AKA Paul Chapman. Developing a prototype [[metamath]] front end in Smalltalk. . . .
1K - last updated 2007-04-11 10:20 UTC by igblan.free-online.co.uk
jcorneli notes on rspuzio July 12 LispNYC talk
=Intro= These are some raw notes I took on the video from Ray's !LispNYC talk. Even though this talk . . . with machine code. [Is this bourn out by Metamath experience?] Basic lisp can be written with . . . that they are applied coherently. Translating metamath database into hcode and checking it! Other . . .
5K - last updated 2005-12-11 00:42 UTC by jcorneli
jorend
Jason Orendorff (myfirstname dot mylastname at gmail). http://jorendorff.blogspot.com/ == Existence of . . . and quickly discovered the reason for this. Metamath defines π as the smallest positive zero of . . . A simply means that A is a set, or [http://us.metamath.org/mpegif/isset.html equivalently] A e. V. . . . The class V [http://us.metamath.org/mpegif/nvelv.html does not exist]. On . . . the other hand, the existence of [http://us.metamath.org/mpegif/df-pi.html pi] is easy to show: . . .
5K - last updated 2008-01-25 06:21 UTC by ocat
latex-test
Is this working yet or what: $$ \int 2x \; dx = x^2 + C $$ It is! It is working!!! $$ \mathcal{P}, \mathbb{R} . . . flag has been set to 1, most of the Metamath pages are broken because of its <nowiki>$d, . . .
3K - last updated 2006-10-31 05:30 UTC by rspuzio
let and double quote
There is no possibility to write let v $123 = "( F " A )". May it be fixed ? -- [[fl]] 22-Dec-2006 *Answer* . . . version 0.07.28 22-Dec-2006 of the [http://us2.metamath.org:8888/index.html#mmprog metamath program], . . .
2K - last updated 2006-12-22 17:05 UTC by norm
mathematical grammar
A while ago I wrote a rather sketchy parser for mathematical expressions. I'm currently about to get . . . romantic math. Start with writing a grammar for Metamath's ZF formulas. I mean strings like "( A e. . . . proper parsing, just with text substitution (Metamath's "e." becames Isabelle's "\<in>" etc.). . . . no need to write the code, yet. You might find metamath.exe's utilities capable for your needs, also... . . . one system to the next (latex is different from metamath ascii shorthand, which may differ from ghilbert, . . .
11K - last updated 2006-12-06 22:54 UTC by jcorneli
metacommons manifesto
=New= Today after considerable delay I released a copy of the "metacommons manifesto" on !PlanetMath, . . . online, without violating copyright law. Metamath is a long-running project in formalized mathematics . . .
25K - last updated 2008-04-22 16:58 UTC by jcorneli
metamath
=Quick Links= * [[metamathMathQuestions|Questions for Norm about Math in Metamath]] ** [[set.mm_discussion_replacement]] . . . - set.mm is a set theory database written in the Metamath language ** ([[set.mm discussion]] - obsolete . . . in a proof * [[Natural deduction based metamath system]] * [[metamath program discussion]] . . . * [[metamath website issues]] * Related projects discussed . . . wiki, roughly sorted by increasing distance from Metamath ** [[mmj2]] - Metamath proof verifier (written . . .
65K - last updated 2008-06-19 10:03 UTC by norm
metamath-Grammars
Grammars extracted from Metamath databases by mmj2 (6/26/2005 versions of files). I thought these might . . . polish notation. In spite of the fact that Metamath files may use parentheses and function symbols . . .
9K - last updated 2005-08-07 04:41 UTC by ocat
metamath-SyntaxAxioms
(Warning: these comments are not authoritative or approved by the inventor of Metamath. In fact, everything . . . I say is false :)) Back in my early Metamath *daze* (bewilderment and confusion), I re-proved . . . my own parser... Conversely, as we see in Metamath's miu.mm database, it is possible to "prove" . . . $. like this: $( wxy $a wff x y $. $) Then rerun Metamath "verify proof *" and see if all of the proofs . . . hypothesis or assertion.) Interestingly, in Metamath, notation schemes are entered as axioms ($a . . .
4K - last updated 2005-08-08 19:14 UTC by ocat
metamath-mmj2DirectoryStructure
=mmj2 Directory Structure= The following directories are empty when downloaded, and are later created . . .
2K - last updated 2005-08-25 03:12 UTC by jcorneli
metamathAndHdmPhaseI
* [[MMHDM1 inspirational quote]] * [[MMHDM1 introduction]] * [[MMHDM1 objectives]] * [[MMHDM1 design . . .
1K - last updated 2005-09-22 23:04 UTC by jcorneli
metamathCalculationalProofs
= SHOW PROOF /CALCULATIONAL = An idea that I had some time ago is to output Metamath proofs as 'calculational . . . this kind of proof automatically from every Metamath proof. I don't think I'll ever have time to . . . Hmm, a Haskell module to parse and verify Metamath proof databases; see http://www.solcon.nl/mklooster/repos/hmm/. . . . to derive calculational proofs from existing Metamath proofs. --[[marnix]] : I like the fact that . . . proofs much more readable than the style on the Metamath site. And they are more complete than the . . .
13K - last updated 2005-11-26 18:52 UTC by c-24-60-119-208.hsd1.ma.comcast.net
metamathGrammarFacilities
(Caution: serious ruminating below! This is amateur hour stuff so don't take any wooden nickels!) Metamath . . . It is part of the engineered simplicity of Metamath that these syntax constructors are defined . . . grammar is constructed, and the fact that the Metamath specification does not explicitly cover derivation . . . the number of grammatical type codes in a Metamath file. Here is a classic example from Schmidt's . . . = 17 ? or 2 + 3 * 5 = 30 ? Recent spin-offs from Metamath such as Ghilbert and Bourbaki implement expressions . . .
15K - last updated 2005-10-28 18:20 UTC by norm
metamathMathQuestions
Hopefully, Norman Megill will wander by and answer [[metamath]] questions :) ----- ==Appendix 4: A Note . . . understand what Norm is saying in http://us.metamath.org/mpegif/mmset.html, Appendix 4, about soundness. . . . As opposed to "simple substitution" (like Metamath's built-in rule), which blindly replaces variables . . . formal proof (at the extremely detailed level of Metamath) they can be tedious and distracting. There . . . equivalence when x and y are distinct (http://us.metamath.org/mpegif/sb5.html): (Note: I am being lazy . . .
138K - last updated 2008-02-24 21:52 UTC by norm
metamathModuleMetadata
Here is the proposal I sent to Norm Megill about adding "metadata" statements to .mm files such as set.mm . . . or HCodebert. I recommend downloading the latest metamath.zip to see set.mm's newest statements. (Uppercase . . . Now is the time to provide input! http://us2.metamath.org:8888/index.html#downloads Also check out . . . which constructs a set of Grammar Rules from Metamath syntax axioms and deals with combinations . . . set of metadata to add to set.mm, in the form of Metamath comments that begin with "$( <MM>". . . .
7K - last updated 2005-09-17 18:47 UTC by ocat
metamathProofAssistantMetadata
NOTE: This is *proposed*. Here is my latest conception, a format for "batch" proof assistant input that . . . assistant would attempt to construct a real Metamath proof. In theory the student might not know . . . above demonstates the concept and shows how Metamath.exe stored the real proof, leaving the metadata . . . that may not presently fit into the scheme for metamath.exe but may be add-ons used elsewhere, thus . . . enhancing Metamath's usefulness. --[[ocat]] 24-Sep-2005 . . .
3K - last updated 2005-09-25 01:39 UTC by ocat
metamath bugs
Please go on to Bugs#metamath_bugs. . . .
1K - last updated 2005-05-05 05:09 UTC by planetx.cc.vt.edu
metamath feature requests
Please go on to Feature_Requests#metamath_feature_requests. Testing a change to the "metamath feature . . .
1K - last updated 2005-11-26 18:57 UTC by norm
metamath program discussion
NOTE: to update this wiki your Username must be "whitelisted" by Aaron. For the purposes of discussion . . . about Metamath or mmj2 I authorize you to use Username "ocat" . . . 23-Nov-2007 ----- While the current rage in [[metamath|Metamath]] software is [[mmj2]], now and then . . . come up for tweaking the stodgy [http://us.metamath.org/index.html#mmprog original metamath program]. . . . added this page to discuss them. == Tooltips on Metamath web pages == Based on a suggestion by Reinder . . .
5K - last updated 2007-11-23 17:33 UTC by ocat
metamath tasks
1. Obtain free "mmj2" source code and documentation. mmj2 provides proof verification and grammatical . . . parsing (syntactic analysis) of arbitrary Metamath ".mm" databases (with only minor restrictions . . .
1K - last updated 2005-08-29 23:20 UTC by ocat
metamath utilities and links
= Metamath utilities and links = _About this page_ This page is intended to host utilities, links and . . . other 'supporting' materials which help the Metamath and friends users. _RSS feed for recent proofs_ . . . In order to support my Metamath reading habits, I've created an RSS feed for . . . new Metamath theorems as they appear in Norm's recent proofs . . . added a link to your RSS feed on the [http://us2.metamath.org:8888/mpegif/mmrecent.html mmrecent] page. . . .
3K - last updated 2006-11-29 14:34 UTC by marnix
metamath website issues
This page can be used to discuss technical problems with the Metamath website and mirrors. ----- =us2.metamath.org . . . problem= There is a problem with us2.metamath.org: it is unavailable half of the time. And . . . = 13:15 UTC = 09:15 EDT. Is the problem that us2.metamath.org didn't respond, or that the domain name . . . instead of http://us2.metamath.org:8888 and let me know what happens? Does . . . --[[ocat]]. For the time being, the http://gr.metamath.org mirror will be updated daily starting . . .
12K - last updated 2008-06-26 15:30 UTC by norm
mmide
I am working on a Python program with a graphical user interface for the Metamath system. It works on . . . use to you in your endeavour feel free to ask. Metamath is a very interesting project... --[[ocat]] . . .
1K - last updated 2006-08-12 07:47 UTC by whale
mmj2
=Next mmj2 Release: Step Prover= [[mmj2StepProver]] -- ETA unknown, hoping for no later than 1-Apr-2009. . . . [http://us2.metamath.org:8888/ocat/mmj2/StepProverDoc.zip StepProverDoc.zip] . . . version of mmj2 uploaded: 1-Aug-2008! http://us2.metamath.org:8888/ocat/mmj2/mmj2.zip = 1,534,041 bytes . . . (don't neglect to check the http://us2.metamath.org:8888/ocat/mmj2/mmj2.md5 ). Refer to mmj2\CHGLOG.TXT . . . is that it provides the effect of updating a Metamath .mm file with your mmj2 Proof Worksheets developed . . .
5K - last updated 2008-11-09 15:09 UTC by ocat
mmj2-01-Oct-2007ReleaseEnhancements
back to [[mmj2]] These all seem like "nice-to-have" features, but they do not seem to more mmj2 forward . . . "No"). If set to "Yes" the generated RPN-format Metamath proofs generated by the Proof Assistant GUI . . . will be in Metamath "compressed" format (see Metamath.pdf). ----- . . . a new proof to the proof already in the input Metamath (.mm file) database. Comparison metrics will . . . set.mm's listed criteria, for inclusion in the Metamath database. The metrics to be computed and output . . .
4K - last updated 2007-08-05 03:33 UTC by ocat
mmj2ASCIITypesetting
back to [[mmj2]] ----- Comments? Following is a brief sketch of my ASCII typesetting plan for use with . . . mmj2 Proof Assistant GUI. Problem: to render a Metamath formula using ASCII ======= in a way that . . . MathML, etc. Strategy: ========= Because Metamath accomodates infix, postfix prefix and combinations . . . to satisfy all users of all varieties of Metamath databases. Therefore, a default scheme shall . . . default ASCII typesetting method for an input Metamath file. In addition, the user shall be able . . .
8K - last updated 2006-05-19 00:38 UTC by ocat
mmj2BetaRelease01Sep2007Feedback
=mmj2 Beta Release 01-Sep-2007 Version= http://planetmath.cc.vt.edu/~mmj2/mmj2jar.zip unzip to a temp . . . algorithm in StepUnifier.java differs from the Metamath.exe PA because mmj2 knows the parse tree of . . .
7K - last updated 2007-07-17 12:48 UTC by ocat
mmj2Feedback20080113
Back to: [[mmj2]] =note about the wiki= NOTE: To update the wiki your "username" must be whitelisted. . . . as precisely as possible to report, "invalid Metamath token", or "token invalid as a variable name", . . . * mmj2 attempts to be absolutely faithful to the Metamath.pdf specification. It validates *every* Metamath . . . syntax rule and implements every feature of the Metamath language. For example, mmj2 implements "include . . . mmj2 is, in fact, more punctilious about the Metamath.pdf syntax rules than metamath.exe :-) Other . . .
24K - last updated 2008-01-14 05:13 UTC by ocat
mmj2FeedbackV20061101
Back to: [[mmj2]] Questions/Comments About mmj2? Here is a dedicated page for feedback about the mmj2 . . . you describe the potential of mmj2 for mapping Metamath code to H-code, once a spec for the latter . . . .mm file to hcode might be as easy as running a metamath.exe command and then feeding the text output . . . would be the objective. A deeper issue is that Metamath and Ghilbert are self-defining and are self-contained. . . . A "mathelogical" system in Metamath/Ghilbert has its own language, symbols, definitions . . .
47K - last updated 2006-11-12 23:31 UTC by ocat
mmj2FeedbackV20070716
Back to: [[mmj2]] Previous version of mmj2Feedback: [[mmj2FeedbackV20061101]] =Questions/Comments About . . . up the Java start-up time. On my 2GHz laptop the Metamath Solitaire applet, with 3000 lines of code, . . . seconds to start up. This is compared to say the Metamath program, which has 30,000 lines of code but . . . Windows machine. (The idea is to have mmj2 and metamath.exe located in the same directory so that . . . and - Copy the following files from C:\metamath into C:\mymmj2: metamath.exe eimm.exe eimmexp.cmd . . .
10K - last updated 2007-07-18 04:09 UTC by ocat
mmj2FutureOf
The 1-Aug-2008 release of mmj2 was the eleventh mmj2 release. A lot has happened since the first release, . . . mmj2 provides many features which make proving Metamath theorems easier, but even after all of the . . . new theorems is still quite difficult, and the Metamath learning curve remains rigorous. ----- One . . . syntax match the internal "abstract" syntax of Metamath statements. This requirement is implicitly . . . imposed by mmj2 but Metamath itself makes no provision for differences . . .
15K - last updated 2008-09-07 18:51 UTC by ocat
mmj2GrammaticalInductiveSets
Some thinking, preliminary to continuing the work on detecting Ambiguity in mmj2. --[[ocat]] 10-Oct-2005 . . . this to an arbitrary grammar generated from a Metamath .mm database such as set.mm requires a change . . . would be cluttered. Instead, the method from Metamath's proof verification engine is used. Substitution . . . of an expression for a variable in Metamath's proof engine is allowed only if the first . . . the first symbol is a grammatical type code that Metamath prepends to every expression. We stipulate . . .
6K - last updated 2005-10-12 03:01 UTC by jcorneli
mmj2InverseProvingProjectIdea
="Inverse Proving" Project Idea= My arduous efforts to reprove hbimd resulted in a shorter proof of hbim, . . . (which I think Norm already knew), that a Metamath RPN-format proof has two levels of structure. . . . "micro" level via its parser, a feature that the metamath.exe program doesn't have. -- [[norm]] To complete . . . of the art software... : On the [http://us2.metamath.org:8888/mmsolitaire/pmproofs.txt Shortest . . . work could be done using RPN; conversion back to Metamath-standard syntax could be done at output-display . . .
28K - last updated 2008-05-10 22:11 UTC by ocat
mmj2ProofAssistantConsiderations
A few untutored, possibly false-to-fact thoughts about the hypothetical new mmj2 Proof Assistant, planned . . . the description of the set is finite)." ----- A Metamath proof is in actuality, a program, that when . . . of the proof. Given that the final label in a Metamath proof *must* yield a single formula on the . . . parsed, which is *not* a requirement of the Metamath specification (see miu.mm!) Now, unless the . . . to the contents of set.mm, and surprise(!), Metamath.exe generated shorter proofs than the hand-coded . . .
5K - last updated 2005-11-09 01:42 UTC by ocat
mmj2ProofAssistantDeriveFeature
(This looks better in html format. it is a throwaway, draft document provided for early review -- pending . . . difficult task :) Motivations: * Typing Metamath formulas by hand is error prone and difficult, . . . formulas. Part of the reason for this is that Metamath has no built-in grammar or syntax beyond the . . . This is a feature, not a bug. The downside of Metamath's agnosticism is that there are no notational . . . -- logical axiom or theorem -- in the input Metamath .mm file. The Ref, together with the associated . . .
23K - last updated 2006-03-15 13:31 UTC by ocat
mmj2ProofAssistantFeedback
Back to: [[mmj2]] =note about the wiki= NOTE: To update the wiki your "username" must be whitelisted. . . . be no "invalid" inputs, which is the way the Metamath Solitaire program works. Unfortunately, I . . . proofs, especially those at the start of a Metamath database (e.g. set.mm or ql.mm) -- as the . . . on the math instead of the label names in the Metamath database. Here are the parameters which I . . .
14K - last updated 2008-10-03 19:26 UTC by ocat
mmj2ProofAssistantFeedback20080113
Back to: [[mmj2]] =note about the wiki= NOTE: To update the wiki your "username" must be whitelisted. . . . I have the tool I always wanted for studying Metamath! Here is one neat thing. Say you want to re-prove . . . Metamath theorems. Like from the beginning. But that . . . of the original mmj2 Unification Search and the Metamath.exe "Derive" + Work Variables features work . . . remember the Ref label that applies. And the Metamath.exe "Derive", which generates the formula . . .
9K - last updated 2008-01-14 05:25 UTC by ocat
mmj2ProofAssistantFeedback20080217
Back to: [[mmj2]] =note about the wiki= NOTE: To update the wiki your "username" must be whitelisted. . . . file or changes to the input .mm file, including Metamath syntax errors or proof verification errors. . . . absolutely great stuff. Give a try: [http://us2.metamath.org:8888/ocat/mmj2/mmj2Beta20080401a.zip http://us2.metamath.org:8888/ocat/mmj2/mmj2Beta20080401a.zip]. . . .
27K - last updated 2008-02-18 01:22 UTC by ocat
mmj2ProofAssistantFeedbackV20060129
=Feedback About the new mmj2 Proof Assistant GUI Version 20060129= The policy here at MMJ2 Research Labs, . . . For someone new to Metamath proving techniques, a good start is to save . . . work through proving them, one by one: http://us.metamath.org/mpeuni/mmtheorems.html If you do not have . . . but as a workaround use the GIF directories at Metamath, like this: http://us.metamath.org/mpegif/mmtheorems.html . . . think the new mmj2 GUI is lots more fun than the metamath.exe Proof Assistant! =Things I like about . . .
37K - last updated 2006-03-29 03:06 UTC by ocat
mmj2ProofAssistantFeedbackV20061101
=Feedback About the new mmj2 Proof Assistant GUI= The policy here at MMJ2 Research Labs, LTD. is to catapult . . . For someone new to Metamath proving techniques, a good start is to save . . . work through proving them, one by one: http://us.metamath.org/mpeuni/mmtheorems.html If you do not have . . . but as a workaround use the GIF directories at Metamath, like this: http://us.metamath.org/mpegif/mmtheorems.html . . . environment.) 4. It does not output proofs in Metamath compressed format. --> This is not impossible, . . .
45K - last updated 2006-11-12 14:50 UTC by ocat
mmj2ProofAssistantFeedbackV20070716
Previous Version of Feedback: [[mmj2ProofAssistantFeedbackV20061101]] =Feedback About the new mmj2 Proof . . . to accomplish the many feats I have observed at metamath.org :-) --[[ocat]] =Installation Grievances= . . . and insert. 2. It does not output proofs in Metamath compressed format. --> This is not impossible, . . . but it is computationally intensive. Given that Metamath.exe now has an import/export facility for . . . to conform as closely as possible to the way the metamath.exe Proof Assistant works with respect to . . .
23K - last updated 2007-07-18 04:05 UTC by ocat
mmj2ProofAssistantQuickTips
==Contents== * mmj2 Proof Assistant Quick Tips * Start-up Speed-up Tip * Quick Tip: mmj2 for Metamath . . . took me when I first started back in 2004 using metamath.exe. Granted, I have done these proofs before . . . (No one can be expected to memorize the 16,000 [[metamath]] statements in set.mm, not even Norm himself...) . . . predicate logic and specify the label of first Metamath statement in predicate logic: LoadEndpointStmtLabel,wal . . . has 123,965 text lines and more than 16,000 Metamath statements. By not loading the entire database . . .
24K - last updated 2008-01-23 08:16 UTC by norm
mmj2ProofAssistantTutorial
[[HomePage]] -> [[metamath]] -> [[mmj2]] -> [[mmj2ProofAssistantFeedback]] -> [[mmj2ProofAssistantTutorial]] . . . LoadEndpointStmtLabel,pm2.521 LoadFile,c:\metamath\expset.mm VerifyProof,* Parse,* RecheckProofAsstUsingProofVerifier,yes . . . Notice the LoadFile command is set to read c:\metamath\expset.mm which contains the contents of set.mm . . . "$=" Generated Proof Step line which shows the Metamath RPN format of the proof. So, I open up my . . . Mozilla browser and display file:///C:/metamath/althtml/mmtheorems.html That is a local copy . . .
9K - last updated 2006-02-02 21:33 UTC by norm
mmj2ProofAssistantUnification
Proof Assistant -- Unification and Metamath Database Lookup Strategy -- An Outline. =A Few Preliminaries= . . . unlikely to yield satisfactory results. However, Metamath is logically "agnostic", and conventional . . . dependent upon the logic or grammar of the input Metamath database -- except to say that the grammar . . . "Ref" values, as on this proof page: http://us.metamath.org/mpegif/isset.html Or, in the format I . . . happy.) ----- ( OFF TOPIC NOTE concerning above Metamath link: (fyi, Ponder theorem "isset" above, . . .
33K - last updated 2005-11-16 05:14 UTC by ocat
mmj2ProofCompressionNotes
=A throwaway page of rough notes= A now obsolete theorem in set.mm, "climadd2OLD" has a proof that expands . . . to approximately 15,000 steps (in Metamath RPN format). As an experiment I used metamath.exe . . . There are other tasks involved in compressing a Metamath proof, and I won't go over all that right . . . array of numerically compressed symbols in the Metamath.pdf format. For metamath.exe the *price* of . . . compression is definitely "worth it" because metamath.exe processes compressed proofs directly in . . .
7K - last updated 2006-03-21 01:27 UTC by ocat
mmj2ProofDerivationMethods
Regrettably, the new mmj2 Step Selector Search feature is not a magical cure for every proof derivation . . . correctly, but I don't see how to turn it into a Metamath proof! I've used the Fitch method before and . . . been able to translate into Metamath, but this one is stumping me. =pm2.61 |- ( . . . version of the weak deduction theorem [http://us.metamath.org/mpegif/dedt.html dedt] / [http://us.metamath.org/mpegif/elimh.html . . . elimh] can be used. See the [http://us.metamath.org/mpegif/mmdeduction.html Deduction Theorem] . . .
13K - last updated 2008-04-01 20:59 UTC by ocat
mmj2Release20071101
=9-Oct-2007= "Testable"..."beta" version of Release 20071101 available now. ...I just uploaded another . . . mmj2jar.zip and .md5 to http://us2.metamath.org:8888/ocat/mmj2/mmj2jar.zip and http://us2.metamath.org:8888/ocat/mmj2/mmj2jar.md5 . . . "info" message "I-PA-0119 Theorem xyz RPN-format Metamath proof generated!" when Ctrl-U (unification) . . .
2K - last updated 2007-10-09 22:33 UTC by ocat
mmj2Release20071101InitialObjectives
(back to [[mmj2]]) (The MetamathOMDocBridge is now just a gedankenexperiment but there are many things . . . make mmj2's Proof Assistant work a lot more like Metamath.exe's. In addition, certain preparations can . . . I. MAKE PROOF ASSISTANT GUI "DERIVE" MORE LIKE metamath.exe 1. Handle $d errors in a more sophisticated . . . etc. were successfully parsed as variables, in metamath.exe they are treated as expressions, that . . . proof in place of each occurrence of $11. And metamath.exe can treat $11 as an expression during . . .
142K - last updated 2007-07-06 07:24 UTC by ocat
mmj2Release20080201
back to [[mmj2]] or [[ocat]] NOTE: use Username "ocat" at bottom of page to update the wiki if the wikilord . . . the VerifyProofs logic (which implements the Metamath Proof Verification specification). An example . . . mmj2 chooses optional variable 'y' whereas the Metamath proof uses variable 'f' (for semiotic reasons.) . . . /need/ coupled with desire. For example, since Metamath theorem proofs are equivalent to computer . . . --[[ocat]] ::: The literate version of Metamath exists: "Elements of Mathematics" N. Bourbaki . . .
31K - last updated 2008-01-07 20:49 UTC by ocat
mmj2Release20080801
I have begun coding for a new version of mmj2. (Tenatively scheduled now for 20080901...) Here is an . . . information about the new release: [http://us2.metamath.org:8888/ocat/mmj2/TheoremLoaderOverview.zip . . . a foundation for other, non-mmj2 code to access Metamath data and mmj2 facilities. The primary use . . . envisioned is extracting Metamath data, as the mmj2 Service feature provides . . . an operational Proof Assistant, with all of the Metamath data fully loaded, parsed and verified. So . . .
45K - last updated 2008-08-18 02:18 UTC by ocat
mmj2SampleOutputTMFF
(back to [[mmj2]]) Below is a sample of my new Text Mode Formula Formatting (TMFF) using method TMFFAlignColumn . . . in set.mm are, in increasing size: [http://us.metamath.org/mpegif/mdslmd1lem4.html mdslmd1lem4], . . . [http://us.metamath.org/mpegif/mdslmd1lem1.html mdslmd1lem1], . . . [http://us.metamath.org/mpegif/mdslmd1lem3.html mdslmd1lem3], . . . [http://us.metamath.org/mpegif/5oa.html 5oa], [http://us.metamath.org/mpegif/5oalem7.html . . .
27K - last updated 2006-09-14 02:13 UTC by ocat
mmj2StepProver
=Next mmj2 Release: Step Prover= ETA? 1-Apr-2009? =User-Design Doc= [http://us2.metamath.org:8888/ocat/mmj2/StepProverDoc.zip . . . is descending order by formula length (number of Metamath math symbols), and in the case of a tie, the . . .
4K - last updated 2008-11-13 07:19 UTC by ocat
mmj2UnificationHintsPreview
(back to [[mmj2]]) =Preview of new MMJ2 Unification Hints Feature= mmj2's Proof Assistant will display . . . an Assertion (axiom or theorem) in the loaded Metamath file(s). ----- I-PA-0413 Theorem cdj3 Step . . .
3K - last updated 2006-09-14 02:14 UTC by ocat
mmj2UnifyingOverloadsFix
Hi Norm, re: /mmj2UnifyingOverloads Short answer: let's use syntax . . . eliminates the class parse of "x = y" but the Metamath Proof Assistant does not, meaning that although . . . proofs use ambiguous parses for "x = y", etc. Metamath's proof assistant is sneaky and does that . . . LoadFile,c:\metamath\expsetTEST20060120v2.mm *LoadFile,c:\metamath\expset.mm . . .
13K - last updated 2006-01-22 17:08 UTC by ocat
mmj2slawekk
Here is an excerpt (partial) from mmj2 RunParm command PrintSyntaxDetails. It shows the grammar rules . . . formula option anyway...) ------ Thanks for the Metamath formulas grammar. That is exactly what I needed. . . . I have one more question. In Metamath when one writes p /\ q /\ r , is this the . . . than my ad-hoc parsing of the output of Metamath show theorem, show proof commands. And learning . . . know how you would handle cases like translating Metamath's "X e. V" to Isabelle's "X = X" or Metamath's . . .
14K - last updated 2006-12-09 05:18 UTC by ocat
mmj3ReengineeringOfmmj2
back to [[mmj2]] =mmj3 - A Re-engineering of mmj2= The 1-Mar-2008 release of mmj2 is working beautifully . . . to honor the logical entities that make up a Metamath database. In mmj2 each MObj is reused, so . . . one instance of "ax-mp", etc. In reality, the Metamath statements that define these mathematical . . . to say that there is only one "ph" variable in a Metamath database because the different occurrences . . . ought to be very easy. I've always believed that Metamath would be just as interesting to Computer Scientists . . .
8K - last updated 2008-05-12 20:37 UTC by ocat
mmjbert
Well! I am finally starting to really "dig" Ghilbert. I like many things about it very much. So I am . . . with direct convertability between it and Metamath. This means another flavor of Ghilbert, which . . . revert to being just Axioms, as they are in Metamath. I believe I see what the intent is for Ghilbert . . . that is "ok" too, except that it will not fly in Metamath, which is what mmjbert must service. Metamath . . . of programming languages. Unfortunately, the Metamath Proof Verification Engine algorithm cannot . . .
37K - last updated 2008-05-22 01:21 UTC by norm
natded20060223.mm
$( <MM> <MODULE> <ID>NATDED</ID> <PREREQ> </PREREQ> </MODULE> . . . Metamath source file for elementary symbolic logic . . . deduction are presented as theorems without Metamath proofs -- initially, the proofs are provided . . . can be independant from the formulas but with metamath you have to append it to your formulas. -- . . . transported into a Hilbert-style system (i.e. Metamath) without use of Contexts? --[[ocat]] :: But . . .
4K - last updated 2006-02-24 21:08 UTC by ocat
next steps for HDM project
After our essentially groundbreaking meeting, I'm left wondering what the next steps for the HDM project . . . example of mathematics. * try to understand Metamath and closely related programs. * import APM-Xi . . . the Schuam's Algebra project, h-code spec, and metamathematical/theorem-proving research. This is . . .
16K - last updated 2005-10-21 22:17 UTC by jcorneli
norm
Norm Megill Web page: http://metamath.org Current project: [[metamath]] . . .
1K - last updated 2005-09-06 13:16 UTC by norm
operation
An operation is an entity which does not bind any variables and can take arguments. This definition is . . . it seems like we're dropping into fairly metamathematical issues. It is fine to discuss them, . . . point that too much of abstract formal logic and metamathematics can get somewhat unbalanced, so it . . . plan to keep on working out and writing up my metamathematical ideas, especially since it seems to . . . the formal math angle after looking more into [[metamath]]. And I also like your suggestion of the . . .
7K - last updated 2005-05-05 05:11 UTC by planetx.cc.vt.edu
pekuja
Hello, my name is Pekka Kujansuu. I'm a mathematics student at the University of Turku in Finland. I . . . I'm currently looking for some good proofs at [[metamath]]. I will try to pick some simple proofs from . . .
1K - last updated 2005-06-20 15:58 UTC by pekuja
philosophy on AsteroidMeta
Joe, from the recent changes log I get the feeling you are getting interested in philosophy of science . . . way down as needed; getting the philosophical/metamathematical basis of hcode worked out seems a . . .
4K - last updated 2005-06-25 17:25 UTC by jcorneli
port metamath to something our ai will like
I think that ghilbert may be even better for us, but it is not explicitly free. So one task is to * [[see . . .
1K - last updated 2005-05-05 05:11 UTC by planetx.cc.vt.edu
raph
I've been hacking on [[metamath]] and my own variant of it, [[Ghilbert]]. My main blog is at: http://advogato.org/person/raph/ . . . topology theorems, and he assigned [http://us.metamath.org/mpegif/cnsscnp.html cnsscnp], [http://us.metamath.org/mpegif/cncnp.html . . . metcn (below). As you can see from [http://us2.metamath.org:8888/mpegif/mmrecent.html mmrecent], I . . .
3K - last updated 2006-11-22 19:56 UTC by fl
response to elephant
= Response to "Elephant" == by Joe Corneli and Aaron Krowne = Introduction = You can get this article . . . to be run. This sort of practical sociocultural metamathematics is well within our grasp. ---- =Discussion= . . .
10K - last updated 2005-07-11 02:31 UTC by rspuzio
sandbox
!DeletedPage $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# "Sandbox" . . . ` Cat ` . That sort of trick is intended to help Metamath which doesn't like too large definitions. . . . ` Cat ` . That sort of trick is intended to help Metamath which doesn't bear the too large definition . . .
132K - last updated 2007-10-26 21:23 UTC by ocat
scholia and literary machines
I've been reading the book Literary Machines by Theodor Nelson - and I'm excited to find ''bascially . . . heavily on the success of existing projects like Metamath. I'm also consciously following the template . . . heavily on the success of existing projects like Metamath. Same here! The two successes which I am bulding . . .
37K - last updated 2006-11-25 18:58 UTC by raph
set.mm discussion replacement
This page discusses various topics and subprojects in set.mm (the set theory database for [[metamath]]). . . . was deleted, so I'll rewrite it for [http://us2.metamath.org:8888/mpegif/ac9s.html ac9s]. : The class . . . also a discussion about this in the [http://us2.metamath.org:8888/mpegif/mmnotes.txt mmnotes.txt] for . . . regarding the similar situation in [http://us2.metamath.org:8888/mpegif/sumeqfv.html sumeqfv], which . . . not free in F is then deduced from [http://us2.metamath.org:8888/mpegif/hbopab1.html hbopab1]. In . . .
70K - last updated 2008-05-18 16:37 UTC by norm
set.mm discussion replacement backup
This page discusses various topics and subprojects in set.mm (the set theory database for [[metamath]]). . . . was deleted, so I'll rewrite it for [http://us2.metamath.org:8888/mpegif/ac9s.html ac9s]. : The class . . . also a discussion about this in the [http://us2.metamath.org:8888/mpegif/mmnotes.txt mmnotes.txt] for . . . regarding the similar situation in [http://us2.metamath.org:8888/mpegif/sumeqfv.html sumeqfv], which . . . not free in F is then deduced from [http://us2.metamath.org:8888/mpegif/hbopab1.html hbopab1]. In . . .
52K - last updated 2007-06-14 23:49 UTC by grumpy dog
steverod
Since March 2006 I have contributed some theorems to the [[set.mm discussion|set.mm]] database for [[Metamath]], . . . including [http://us.metamath.org/mpegif/demoivre.html De Moivre's Formula]. . . . epsilon relation ~ df-eprel , respectively) in Metamath, we instead use ` A ` to represent _V_, the . . . epsilon relation ~ df-eprel , respectively) in Metamath, we instead use ` P ` to represent _V_, the . . . the benefits of this approach in the [http://us.metamath.org/mpegif/mmnotes.txt mmnotes.txt] entry . . .
11K - last updated 2007-01-29 18:17 UTC by steverod
ufomath
This is a page about ufomath (http://ufomath.wikispaces.com). Moving some discussion here from [[alih]] . . . is like [[mmj2]]. It has nothing to do with [[metamath]] proofs - it just calls ATP repeatedly. In . . . the logic part, whereas ocat reimplemented the metamath core in java, and so can use that module instead . . . web pages. I understand that the popularity of Metamath increased dramatically once Norm created the . . . Metamath Explorer web page series. I can also relate . . .
7K - last updated 2006-01-14 12:25 UTC by alih
using template utilities to check proofs
One of the main reasons for writing [[template utilities]] was to provide routines for verifying proofs. . . . of the first few theorems form the [http://us.metamath.org/mpegif/mmtheorems.html metamath list of . . . The names of the results are taken fron the metamath page. [[using template utilities to check . . . needed. (I say maybe "a parser" here because the metamath language might be sort of specialized, and . . . "supposed to be" general.) Maybe we can get this metamath-checking system running w/i about a week? . . .
2K - last updated 2005-05-05 05:18 UTC by planetx.cc.vt.edu
using template utilities to check proofs - a2i
This is based on http://us.metamath.org/mpegif/a2i.html (setq a2i-pr1 '((p q r) (if p (if q r)))) => . . .
1K - last updated 2005-05-05 05:18 UTC by planetx.cc.vt.edu
using template utilities to check proofs - ali
This is based on http://us.metamath.org/mpegif/a1i.html '''Let us "derive" the proof starting with the . . .
3K - last updated 2005-06-19 03:38 UTC by rspuzio
using template utilities to check proofs - axioms
''This is based on the axioms found on the following pages:'' * http://us.metamath.org/mpegif/ax-1.html . . . * http://us.metamath.org/mpegif/ax-2.html * http://us.metamath.org/mpegif/ax-3.html . . . * http://us.metamath.org/mpegif/ax-mp.html Axiom (schemas) are . . .
2K - last updated 2005-05-05 05:18 UTC by planetx.cc.vt.edu
using template utilities to check proofs - id
This is based on http://us.metamath.org/mpegif/id.html (setq id '((p) (if p p))) => ((p) (if p p)) . . .
1K - last updated 2005-05-05 05:18 UTC by planetx.cc.vt.edu
using template utilities to check proofs - id1
This is based on http://us.metamath.org/mpegif/id1.html Back to [[using template utilities to check proofs]] . . .
1K - last updated 2005-06-18 05:30 UTC by rspuzio
using template utilities to check proofs - idd
This is based on http://us.metamath.org/mpegif/idd.html Back to [[using template utilities to check proofs]] . . .
1K - last updated 2005-06-18 05:31 UTC by rspuzio
visions
#REDIRECT [[Metamathematical Visions - metadata, learning, and knowledge communities]] . . .
1K - last updated 2006-01-12 14:59 UTC by jcorneli
visions talk
Metamathematical visions: metadata, learning, and knowledge communities. Let's define the terms, but . . . in some sense, "mathematics" _is_ "learning" and metamathematics is the study of learning. =Knowledge . . . homogeneous medium of clear, logical writing. =Metamathematics= Metamathematics is mathematics used . . . statistics and sociology). When I talk about "metamathematics", I want you to think these things . . . as well as the usual. While usual metamathematics deals with capturing mathematical content . . .
7K - last updated 2006-01-13 19:50 UTC by jcorneli
whale
I am working on a Python program with a graphical user interface for the Metamath system. It works on . . .
1K - last updated 2006-08-11 00:42 UTC by ip24-252-105-196.no.no.cox.net
write or obtain a prover
We will need a system that will convert hcode proofs into formal proofs. (The [[metamath]] proof verifier . . . logic (in fact the first few proofs from the metamath collection) wrote them as s-expressions and . . .
4K - last updated 2005-11-02 21:02 UTC by jcorneli
217 pages found.