Please move metamath 100 results into main body

[David A. Wheeler]

As I recently posted, I believe that all "Metamath 100" results (and thus all they depend on)
should eventually move into the main body. After all, all Metamath 100 results are
results that at least some others believe are important. I suspect the folks who already produced metamath 100 results would be the best situated for proposing where things go.

So: if you produced a metamath 100 result, but it's currently not in the main body, I would love to see your proposals to start moving their dependencies and the result itself into the main body. If there are many parts, I expect that mini case it would be easier to do it slowly in pieces.

There is no rush. That said, I think it's important to keep working on getting more things moved from mathboxes
into the main body. Tools like mmj2 only consider items in the main body for
many automated steps, and in any case I think it's far more sensible to
readers if major results are properly organized in the main body.

--- David A.Wheeler

[Alexander van der Vekens]

Hi David,

I fully agree with you - I also suggested to move all theorems of the mm100 list which are still in mathboxes into the main part of set.mm a long time ago.  If I counted correctly, there are still 10 such theorems in mathboxes: #9, #30, #45, #61, #73 ("part of"?), #77, #83, #87, #88 ("part of"?), #90. I would propose to creare an issue in GitHub for each of them (as I have done for #49, see issue #1333, which will be finished by my recent PR #1361), so that we can track the progress of moving them to the main part. I would start working on the issue for #83 next year ;-).

Alexander

[Alexander van der Vekens]

Oh, I missed the recent #76, which does not have the marking "This is Metamath 100 proof #76" in its comment yet ...

[savask]

As a sort of opposite opinion, I would like to argue that the current convention of moving theorems out of mathboxes (move only if it's used by someone else) should also apply to metamath 100 results.

First of all, metamath 100 theorems are clearly not obscure facts that are hard to find, they are announced in the google group, showcased in the "recent news" on the metamath site and also permanently linked in the metamath 100 list. Now, if some metamath 100 theorem required the development of an important branch of math currently missing from set.mm (matrices or Fourier series, among recent examples), then it should be relatively easy for someone to make use of those theorems and fulfill the current movement criterion. Needless to say, another person might uncover some problem or inconvenience in the new math section, overlooked by the metamath 100 contributor.

In case new theorems are not being used, they can stay in the mathbox without any trouble, in my opinion. It gives the author more time to improve his results, and ultimately can't make them worse. I must agree that theorems in the main body of set.mm are more "well-known" than mathbox results, but I think that the "hype" around metamath 100 theorems is high enough to make people remember where to look if they want to prove something about matrices or Fourier series :-)

As a compromise suggestion, maybe instead of deliberately moving all metamath 100 results into the main body we shall leave it to the contributor of the corresponding theorem? I.e. allow them to move their metamath 100 entry into the main part when (or if) they want. And in case someone wants to see a metamath 100 theorem formalized by another person in the main part, they can always come up with some theorem using the metamath 100 result in question to formally satisfy the movement "rule" :-)

[David A. Wheeler]

On Mon, 30 Dec 2019 00:58:45 -0800 (PST), savask <sav...@yandex.ru> wrote:
> As a sort of opposite opinion, I would like to argue that the current
> convention of moving theorems out of mathboxes (move only if it's used by
> someone else) should also apply to metamath 100 results.
>
> First of all, metamath 100 theorems are clearly not obscure facts that are
> hard to find, they are announced in the google group, showcased in the
> "recent news" on the metamath site and also permanently linked in the
> metamath 100 list. Now, if some metamath 100 theorem required the
> development of an important branch of math currently missing from set.mm
> (matrices or Fourier series, among recent examples), then it should be
> relatively easy for someone to make use of those theorems and fulfill the
> current movement criterion.

it's true that the metamath 100 final results are not "obscure".
However, all the supporting material in mathboxes is *much* less visible
than material in the main body. Their primarily heading level is the name of a person,
instead of their logical position, and in many cases tools ignore those theorems by default.

The "mathbox" construct is very useful. I just think there's a lot of material
in the mathboxes today that should move into the main body.
Different people have different specializations, so not all material that should be
in the main body will "naturally" move up through the "use by two people" rule-of-thumb.

I don't think it needs to be complicated, or have an additional "stage".
If you see stuff in your mathbox that you think is ready to move into the
main body, please make pull request(s) that moves groups of that
work into logical places. Some requests will get some pushback, and others
will be "sure, that makes sense".

...

> As a compromise suggestion, maybe instead of deliberately moving all
> metamath 100 results into the main body we shall leave it to the
> contributor of the corresponding theorem?

In general I agree with that, in the sense that the person who created the
proof probably has additional insight into "where it goes" in the main body.
But I want to encourage people to do so. Not all such proposals will be
accepted, but then there can be a reasonable discussion.

--- David A. Wheeler

[savask]

...

However, all the supporting material in mathboxes is *much* less visible
than material in the main body. Their primarily heading level is the name of a person,
instead of their logical position, and in many cases tools ignore those theorems by default.

I fully agree that mathboxes material is not that often looked at, but it's not hidden in any way either. If someone is eager to contribute to set.mm, they will surely find about mathboxes and material in there. As for tools ignoring mathbox theorems, it's a problem of our proof assistants not of set.mm organization, in my opinion.

The "mathbox" construct is very useful. I just think there's a lot of material
in the mathboxes today that should move into the main body.
Different people have different specializations, so not all material that should be
in the main body will "naturally" move up through the "use by two people" rule-of-thumb.

My point is, if the material is not going to be used by anyone but the author, is it worth moving it into the main part? If someone were, for instance, to formalize the four color problem in metamath, would it be worth putting such a piece of highly specialized mathematics into the main body of set.mm? Of course it's a stretch, but in my opinion if the area is important (and, so to say, fundamental) enough, it should be relatively easy to fulfill the current movement rule. For example, that also settles the tooling question: if you suffer from your proof assistant not suggesting mathbox theorems, then you've found a good use for those theorems, and they can be happily moved into the main body.

I don't think it needs to be complicated, or have an additional "stage".
If you see stuff in your mathbox that you think is ready to move into the
main body, please make pull request(s) that moves groups of that
work into logical places. Some requests will get some pushback, and others
will be "sure, that makes sense".

That is, perhaps, my main concern. The current rule leaves almost no place for objections or disputes, while the idea of something "being ready to be in the main body" is quite broad. There might be different views on how certain conceptions should be formalized, and I think the most fair way to rule out such situations is by showing your support: if someone but the author is eager to use new results and conceptions then they are not useless and accepted by, at least, two people.

I agree that often it's favorable to move some mathbox results into the main part without waiting for someone to utilize them, but I don't think it should be done often. Metamath 100 contributions indeed frequently touch important math areas and I fully support the idea of moving these "chunks" of theory into the main body (if the respective contributor is okay with that), but I'm not sure if the same practice should be adopted for other seemingly important results.

[David A. Wheeler]

On Mon, 30 Dec 2019 10:04:53 -0800 (PST), savask <sav...@yandex.ru> wrote:
> I fully agree that mathboxes material is not that often looked at, but it's
> not hidden in any way either. If someone is eager to contribute to set.mm,
> they will surely find about mathboxes and material in there. As for tools
> ignoring mathbox theorems, it's a problem of our proof assistants not of
> set.mm organization, in my opinion.

It's not a *problem*, it's an intentional choice and IIRC it represents an
intentional *change* from how some tools used to work. Because tools can't figure out
how "baked" stuff in the mathboxes is, some tools avoid mathbox material entirely
unless it's specifically requested.

But a lot of the mathbox material *is* ready to be moved into the main body.
It's really a *social* problem that some isn't being moved in, and I hope to
speed things along for the relatively small set of theorems related to these 100 theorems.

> My point is, if the material is not going to be used by anyone but the
> author, is it worth moving it into the main part?

I think that confuses cause & effect. A lot of material in mathboxes won't
be used by other authors because the tools don't point to the material in mathboxes.
Thus, the material that *should* trigger the rule never trigger the "used by two people" rule.

> If someone were, for
> instance, to formalize the four color problem in metamath, would it be
> worth putting such a piece of highly specialized mathematics into the main
> body of set.mm?

I would say, "of course it should be in the body".
Almost all mathematics is "highly specialized" by some definition
once you move beyond 2+2=4. I believe that most working mathematicians
are also highly specialized by almost any definition.
Also, even if a particular Metamath 100 theorem is unlikely to be reused directly,
I think a vast majority of the materials that the proofs are *based* on are
likely to be reused, so let's get them in the body.

Personally, I don't expect that particular question to show up for a while anyway.
I hear the four-color proof is on the large side :-).
That said, there *is* a proof using Coq
("Formal Proof—The Four-Color Theorem" by Georges Gonthier,
https://www.ams.org/notices/200811/tx081101382p.pdf ).
I don't know if that Coq proof would work in the current version of Coq
(I would love to know either way!). The proof is public, but the
last changes to make it work with an updated Coq date back to 2011. See:
https://github.com/kik/Four-Color-Theorem-Maintenance
And yes, I'd love to see a Metamath proof.

To be fair, at the most there are 100 proofs in "Metamath 100".
So this is really only about a very small set of theorems, compared to all
theorems people may consider. No matter what,
we need to continuously move fully-baked material from mathboxes
to the main body over time as those materials are ready.

I just think that encouraging this to happen with the Metamath 100 theorems
will have the happy result of encouraging some important areas
to be filled into the main body more quickly than they would otherwise.

--- David A. Wheeler

[Thomas Brendan Leahy]

An issue I have is I wonder whether it would also make sense to move my *nc theorems to the main box, since the definition of area implicitly implies on the axiom of countable choice - or not.  A complication is that while I'm working on the Poincare-Miranda theorem, I notice that getting it to the Brouwer fixed point theorem would probably most easily entail the theorem that an open star domain is homeomorphic to the whole space, and the simplest proof of that would probably involve FTC.  So now we've got a "100" theorem that (unlike areacirc) doesn't use analysis language, relying on countable choice through analysis theorems.

[fl]

I fully agree that mathboxes material is not that often looked at, but it's not hidden in any way either.

The problem is not that it is hidden, the problem is that it is not ordered and therefore it's harder to find. Beyond logic and the elementary

theorems of set theory people use the headings as a clue to find the theorems they need.

Moreover there may be several different formalization of the same concept. One must choose one.

Someone suggested using Bourbaki as a guide for ordering the definitions 

and theories related to structures. I think this is a good idea. 

It is the longest and most comprehensive treatise on structures.

-- 

FL

[Benoit]

On Saturday, January 11, 2020 at 1:52:55 PM UTC+1, fl wrote:

Someone suggested using Bourbaki as a guide for ordering the definitions 

and theories related to structures. I think this is a good idea. 

It is the longest and most comprehensive treatise on structures.

You probably refer to our discussion: https://groups.google.com/d/msg/metamath/XuIC0pfgs1w/O0cgC94bBAAJ

Benoît

 

[fl]

 

You probably refer to our discussion: https://groups.google.com/d/msg/metamath/XuIC0pfgs1w/O0cgC94bBAAJ

Yes. 

-- 

FL

[fl]

Someone suggested using Bourbaki as a guide for ordering the definitions 

and theories related to structures. I think this is a good idea. 

It is the longest and most comprehensive treatise on structures.

It's a good idea. I insist.

Netflix streaming when the planet is burning is a bad idea, but Bourbaki is a good idea. 

Buying food with palm oil when the forests of tropical countries are destroyed by odious capitalist companies 

is a bad idea, but Bourbaki is a good idea. 

Taking the plane for one's leasures when the ecosystems are systemtically destroyed it is a bad idea but Bourbaki it is a good idea.

Don't be passive, have a walk on the side of the good ideas!

-- 

FL

[fl]

Guys once again. Do something for the planet: renounce to netflix and your smartphones and adopt Bourbaki.

Your children and grandchildren will look up to you as heroes and not as those who did nothing.

-- 

FL

[vvs]

Guys once again. Do something for the planet: renounce to netflix and your smartphones and adopt Bourbaki.

Your children and grandchildren will look up to you as heroes and not as those who did nothing.

I don't like smartphones, don't watch Netflix and I'm trying to learn something new and interesting here. Am I a hero? Hmmm...  Seems like everyone else takes me for some kind of nerd or something.

I have no opinion about Bourbaki, though. That might be the problem... Also, I'm probably too old and conservative for generation Z and pretty cynical. Also, I think that trying to save the world is a mistake, because it doesn't want to be saved. But I like people as a culture, their good sense of humor and don't like robots and transhumanism, but someone would call me a misanthrope at the same time.

Though, you should ignore me, because I'm a grouchy oddball.

[fl]

 

Though, you should ignore me, because I'm a grouchy oddball.

Don't be so negative. You don't like smartphones and don't watch Netflix: you look like a very brave man. Your grandchildren will show off proudly your photograph 

in their atomic shelter to their relatives as THE guy who did something.  For Bourbaki it is simple, we need to have a common base to synchronize ourselves.

Bourbaki has a comprehensive treatment of the structures  of all kinds. This seems to be a very good tool for synchronization.

-- 

FL

[Jim Kingdon]

On January 12, 2020 10:17:49 AM PST, vvs <vvs...@gmail.com> wrote:
>I have no opinion about Bourbaki, though. That might be the problem...

Heh, maybe it is a generational thing because I look at the HoTT book as the thing to be studied and formalized.

Like Bourbaki, it was written by a number of collaborators (even I contributed a sentence via pull request). Like Bourbaki it aims to summarize and systematize mathematics.

Now, it covers far fewer topics than Bourbaki and I'm not even sure what I think about the premise of the book (type theory in general, or univalent dependent type theory in particular) or certain topics (e.g. surreal numbers).

But I guess I understand the nerdy impulse to read math books (or write metamath proofs) rather than, say, keep up with the latest TV series.

[Benoit]

On Sunday, January 12, 2020 at 11:51:10 PM UTC+1, Jim Kingdon wrote:

Heh, maybe it is a generational thing because I look at the HoTT book as the thing to be studied and formalized.

Please note that Bourbaki was not brought up in this discussion (in the link I gave above) as the thing to be studied and formalized, but merely because its TOC could serve as a guide for ordering the sections of set.mm.

Benoît

[fl]

Heh, maybe it is a generational thing because I look at the HoTT book as the thing to be studied and formalized.

HoTT is a small book compared to the one by Bourbaki. I don't know what's in it anymore (type or category theory) 

but in my opinion it will be as usual: it will not supplant the other points of view, but it will be added to the others. 

If you take a book by Knuth, you'll notice that his favorite style of math is 19th century math, 

and that's interesting. If you take the formalization of typed lambda calculus, you will soon notice that they 

quickly jump to formalized set theory in this new framework. 

And Benoît recalls in the post just above that he just wants to use Bourbaki's treatise table of contents. No more.

-- 

FL

[fl]

HoTT is a small book compared to the one by Bourbaki. I don't know what's in it anymore (type or category theory) 

And if it's about category theory -- what can I say! -- it presupposes knowing what a structure is. I guess. 

-- 

FL

[fl]

I think you can even still make proofs in the style of Euclid, it will be accepted (if relevant).

-- 

FL

[fl]

Thank you to vvs and Kingdon for their posts. It was very kind of them.

-- 

FL

[vvs]

Thank you to vvs and Kingdon for their posts. It was very kind of them.

You are welcome. I just don't afraid to look ridiculous, but I have nothing to lose anyway.

BTW, I wonder if Bourbaki is the only place for proper taxonomy? Shouldn't there be established standards, similar to MSC2010? As I've said in other thread: why not have some formal classification and let the user to assign his own tags for searching. That would need better tools of course.

[fl]

BTW, I wonder if Bourbaki is the only place for proper taxonomy? Shouldn't there be established standards, similar to MSC2010? As I've said in other thread: why not have some formal classification and let the user to assign his own tags for searching. That would need better tools of course.

It's not the same thing. The MSC2010 is just a list of topics. It is used to classify math articles as the Dewey Decimal Classification is used by librarians to

classify the books. In Bourbaki's treatise, at least in the first six volumes, a theorem depends only on what is found in the previous volumes. 

There is no such thing in MSC2010.

And above all it permits to find a core of mathematics. Because mathematics by themselves 

-- 

FL

[fl]

And above all it permits to find a core of mathematics. Because mathematics by themselves 

Above all, it permits us to define a subset of theorems that we can consider as the heart of mathematics.

 Because mathematics, all the same, are pervasive. The first six books of the treatise have shown 

in practice that they constitute an acceptable core.

Because of the structure of set.mm we have to remain linear. No network structure is possible.

-- 

FL

[fl]

 

 

Also, I think that trying to save the world is a mistake, because it doesn't want to be saved. 

 https://www.francetvinfo.fr/meteo/climat/le-pdg-de-total-juge-que-le-debat-sur-la-crise-climatique-est-trop-manicheen_3784583.html

Terrifying. Absolutely terrifying. Capitalism: the ultimate predator.

-- 

FL

[vvs]

Terrifying. Absolutely terrifying. Capitalism: the ultimate predator.

I'm sorry, that the life could be frustrating. But every human is his worst enemy. Just as nobody forced people to live that way, you are not forced to scare people away. Do you think this forum is a good place to ask such questions? Or is it even appropriate place? Aren't you seeking simple answers to complex philosophical questions? BTW, every good idea can be reduced to absurdity and nothing good will come of it. Every man on this planet should do what he is good at. That's my idea of what the good is. I believe that people here have a conscience but they came here with the particular goal to become good at formal proofs and this is already hard enough. Please, don't ask too much from them.

I have infinite patience and I like philosophy, but I can't speak for everybody else. Ask yourself: do you support political activities over studying mathematics in universities? I heard of some professors who lost their jobs because of that. And I think that some people could be nervous and that is not a good way to attract attention. Why not join some ecological or social movement and be more effective then? Why not use pedagogy on youth at school and home?

That's just my personal opinion and you can always ignore it, of course. Write me in private mail if you like a good conversation. I'm always glad to chat with you or anybody else.

[fl]

Do you think this forum is a good place to ask such questions?

It wasn't a question. It's a affirmation. And you're right, this isn't the right place. You're a wise man, and not just because you don't watch Netflix and don't have a smartphone. I'm sure we should put the photo of the smartphone's creator in the history books next to Stalin's.

-- 

FL