Though I do have programming experience, it's been a long time. I need to learn how to work with github (something I plan to do anyways for other work).
The kind of application that would really interest me would be one that can utilize routines to construct instances of meta-theorems in raw metamath language. I figure this would reduce the visibility of a lot of boilerplate steps needed employ very instinctual steps like simple substitutions and antecedent rearrangement / matching for natural deduction. In most metamath proofs it seems most of the difficulty in reading comes from the amount of boilerplate that isn't easy to immediately recognize as such. There are a lot of specialized logic theorems to make proofs shorter, but being shorter doesn't make them easier to understand as you end up jumping down deeper and deeper into a wormhole of sub-theorems and lose track of the big picture, in the logical sense. What I'm writing is not directly connected with meta-math, but something that I feel could help explain it better for novices and could be made to match up easily. On Tuesday, July 4, 2023 at 3:11:56 PM UTC-4 David A. Wheeler wrote: > > > > On Jul 3, 2023, at 10:58 PM, Marshall Stoner <[email protected]> wrote: > > > > Thanks. I was not very specific because I was waiting to make sure I was > actually subscribed to the group. I attached the pdf to show you the idea > of what I'm doing. I would like to provide the quickest and easiest way > forward to that start of ZFC theory while still being formally precise. > Like you said, there are far too many theorems to easily convert into a > "book form" that includes everything. > > It's up to you, but one possibility would be create a document in the > set.mm repo > with the name `mmSOMETHING.raw.html`. These are just normal HTML files, > but anything in > `...` is processed by metamath-exe to generate nicer-looking HTML for the > equations. > This is how we generate, for example, mmcomplex.raw.html - this is > processed and > turned into mmcomplex.html for use as a final document. There's no > obligation to use > that mechanism, but you might find it useful. > > I've thought about creating a "tour guide" of sorts that points out and > explains the highlights > (without going into the details of *every* theorem) - it sounds like you > might have a somewhat > similar goal. If it's in the set.mm repo, it can be updated along with > the rest of set.mm. > > --- David A. Wheeler > > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8ffa824a-fdd1-486c-9934-8c3ca00e75d8n%40googlegroups.com.
