Metamath 100 idea

[Norman Megill]

One of the difficulties with many of the mm_100 theorems is figuring out how to state the theorem in the first place.  Sometimes that initial hurdle is enough to discourage people from even considering the problem.  At least it is for me, and I suspect it probably is for others, too.  But once the problem is written down in the Metamath language, it removes any ambiguity or uncertainly as to what the goal is.  This might inspire more people to at least ponder the problem.

The idea is to write down some remaining theorems in the mm_100 list without proof.  A person with some expertise in the area could do this without having to commit to a large amount of time writing the proofs.  This would establish definite goals for others who are willing to invest the time (which is often a good opportunity for them to learn about the topic in a rigorous fashion, as well).

For some theorems, it may be useful to look at the statement proved in other proof languages and even translate them by hand into set.mm notation.

These theorems could be inserted into set.mm in the form of commented-out theorems with empty proofs and $ changed to @.  This way symbols would be updated automatically whenever we change them from time to time.  We could uncomment them every now and then (possibly stated as temporary axioms) to check the syntax with mmj2.  Example:

$(
  @( Fermat's last theorem. @)
  flt @p |- ( ( N e. ( ZZ>= ` 3 ) /\ ( X e. NN /\ Y e. NN /\ Z e. NN ) )
    -> ( ( X ^ N ) + ( Y ^ N ) ) =/= ( Z ^ N ) ) @=
    ? @.
$)

Many problems can't be stated without new definitions, so of course describing or even stating the necessary definitions would be helpful.

Something to think about.

Norm

[fl]

Many problems can't be stated without new definitions, so of course describing or even stating the necessary definitions would be helpful.

 

Sure but to state the area of a circle you need  Euclid's plane definition.

--

FL

[Mario Carneiro]

areacirc is already in set.mm in this form FYI. Euclidean geometry is not required, just a bit of measure theory.

--
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 metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[fl]

I can't find the theorem. But if you always give the proofs in the most cryptic form (measure theory) you won't give anybody

the desire to read you. If you give on the contrary Leibniz's proof with a link to a video that clearly explains how

it was designed (some exist) and with a reference to Euclid's theory. frankly I'm sure you will have readers.

"On n'attire pas les mouches avec du vinaigre" (French proverb)

--

FL

[David A. Wheeler]

On August 24, 2017 8:58:11 AM EDT, Norman Megill <n...@alum.mit.edu> wrote:
>One of the difficulties with many of the mm_100 theorems is figuring
>out
>how to state the theorem in the first place. Sometimes that initial
>hurdle
>is enough to discourage people from even considering the problem. At
>least
>it is for me, and I suspect it probably is for others, too. But once
>the
>problem is written down in the Metamath language, it removes any
>ambiguity
>or uncertainly as to what the goal is. This might inspire more people
>to
>at least ponder the problem.
>
>The idea is to write down some remaining theorems in the mm_100 list
>without proof. A person with some expertise in the area could do this
>without having to commit to a large amount of time writing the proofs.

...

>Many problems can't be stated without new definitions, so of course
>describing or even stating the necessary definitions would be helpful.
>
>Something to think about.

I love this idea! I agree, it'd help people get started, and it'd also help us be more concrete about what needs to be defined.

The statements from other tools, like HOL Light, might help in some cases.


--- David A.Wheeler

[Thomas Brendan Leahy]

One thing that struck me first reading the list was that among the "obvious omissions" was the Jordan Curve Theorem, without which you can't even really state Green's Theorem.

Seeing the commented-out statement of areacirc I realize I've made my life much harder than it had to be... but I'm not starting over (or even closing the program, after what happened last time) now.  (Besides, the point where it would have made a difference beyond a few extra invocations of recl was a few hundred thousand steps ago.)

(It might be excessively cheeky to add "@p |- ( x e. ( ( exp ` ; 1 6 ) (,) +oo ) -> ( abs ` ( ( psi ` x ) - x ) ) < ( ( ( sqr ` x ) x. ( ( log ` x ) ^ 2 ) ) / ( 8 x. pi ) ) ) @= ? @."...)

[fl]

I cant' belive it.

I need to argue for years to get the definition of an Euclid's plane in the official part of set.mm.

But the 8th problem of the 100 theorems list you are so fond of is "The Independence of the Parallel Postulate".

To prove the Independence of the Parallel Postulate you *need* the definition of an Euclid's plane.

Can we add df-polig to the official part of set.mm wo that we can prove the Independence of the Parallel Postulate.

--

FL

[Thomas Brendan Leahy]

I was a bit snarky about this before, but do actually we have anything like a working definition of the interior of a curve?  In particular I'm thinking of 57, Hero(n)'s formula - JCT seems overkill for that one, but using an ad hoc definition such as "the interval between on every abscissa that passes through exactly two points" seems poor form.

Anyway, I was thinking of 16, the Abel-Ruffini theorem - maybe a sequence of formulae, where any is either a rational number, a coefficient of the polynomial, the sum, difference, product, or quotient of two previous functions, or a previous function raised to a rational power, then show that for any set of N > 5 formulae taken from such a sequence there must exist a polynomial of degree N whose roots don't match up?  A little worried about the "quotient" part, but I imagine any divide-by-zero error would take care of itself.

[Mario Carneiro]

On Sat, Sep 2, 2017 at 8:43 PM, Thomas Brendan Leahy <tbrend...@gmail.com> wrote:

I was a bit snarky before, but do we have anything like a working definition of the enclosure of a curve?  In particular I'm thinking of Hero(n)'s formula - JCT seems overkill for that one, but using an ad hoc definition such as "the interval between on every abscissa that passes through exactly two points" seems poor form.

The obvious solution here is to make a definition that is appropriate for the theorem in question. Heron's formula extends to the area of any polygon by a Green's theorem like approach. Piecewise polynomial shapes capture most geometrical figures, but they have an easy JCT because any line can intersect a polynomial only finitely many times unless it coincides with an edge.

That said, I don't think we should shy away from JCT, because it is itself an important theorem and has many many applications, like this.

 

Anyway, I was thinking of 16, the Abel-Ruffini theorem - maybe a series of formulae, where any is either a rational number, a coefficient of the polynomial, the sum, difference, product, or quotient of two previous functions, or a previous function raised to a rational power, then show that for any set of N > 5 formulae taken from such a series there must exist a polynomial of degree N whose roots don't match up?  A little worried about the "quotient" part, but I imagine any divide-by-zero error would take care of itself.

To me, Abel-Ruffini says that if we create the collection S of meromorphic functions f e. ( CC ^pm CC ) (where ( CC \ dom f ) is finite) by taking integer constant functions, the identity function, and close under sums, products, quotients where the second function is not identically zero, and n-th roots, then no function f(a) e. S satisfies f(a)^n + a f(a) + 1 = 0 for all a e. dom f, where n >= 5. (We could use a different polynomial than x^n+ax+1 if it is easier, but this is nicely concrete.) In fact, it should even be provable that f(0)^n + f(0) + 1 =/= 0 for all f in S, which is to say that x^n+x+1 has no definable roots given these building blocks.

You could be more agnostic about the parameterization of the polynomials, by trying to talk about functions f(a0,..., an) giving roots of sum_i e. (0..n) a_i x^i, but this would both make the theorem weaker and require more work to state.

Mario

[Thomas Brendan Leahy]

Do you have a natural-language proof for that version?  The version I gave is indeed weaker (...especially that "N > 5" bit -_-;...), but it follows pretty quickly from the insolubility of S₅.

[Mario Carneiro]

Ah, it looks like I messed up my polynomials a bit -- x^5 + x + 1 factors, so it's not a good choice. What we need is a polynomial with Galois group S5, and x^5 - x - 1 works. (I suspect that x^n-x-1 has Galois group Sn, but that looks to be hard to prove, and most of the example proofs I find on the internet use specific facts about the polynomial and/or small group theory, and as such don't generalize well.) See:

http://www.math.uconn.edu/~kconrad/blurbs/galoistheory/galoisaspermgp.pdf (p.9)

http://www.math.jhu.edu/~smahanta/Teaching/Spring10/Stillwell.pdf

https://math.stackexchange.com/questions/165675/constructing-a-galois-extension-field-with-galois-group-s-n

https://math.stackexchange.com/questions/393646/irreducibility-of-xn-x-1-over-mathbb-q

An intermediate step in the particular formulation I have given, and the generalization I am envisioning, is: If p(x) is a polynomial whose Galois group has S5 as a subgroup, then the collection S mentioned before contains no function f such that p(f(0)) = 0.

Another way to pack up this data is to skip functions entirely. Let C be the least subset of CC containing ZZ and closed under addition, multiplication, inverse, and satisfying x^n e. C -> x e. C for n e. NN. Then x^5-x-1 (or any polynomial with Galois group containing S5) has no roots in C. It follows that there is no formula in radicals for sum_i^n a_i x^i where n >= 5.

Mario

On Sun, Sep 3, 2017 at 12:46 AM, Thomas Brendan Leahy <tbrend...@gmail.com> wrote:

Do you have a natural-language proof for that version?  The version I gave is indeed weaker (...especially that "N > 5" bit -_-;...), but it follows pretty quickly from the insolubility of S₅.

On Saturday, September 2, 2017 at 10:45:35 PM UTC-4, Mario Carneiro wrote:

On Sat, Sep 2, 2017 at 8:43 PM, Thomas Brendan Leahy <tbrend...@gmail.com> wrote:

I was a bit snarky before, but do we have anything like a working definition of the enclosure of a curve?  In particular I'm thinking of Hero(n)'s formula - JCT seems overkill for that one, but using an ad hoc definition such as "the interval between on every abscissa that passes through exactly two points" seems poor form.

The obvious solution here is to make a definition that is appropriate for the theorem in question. Heron's formula extends to the area of any polygon by a Green's theorem like approach. Piecewise polynomial shapes capture most geometrical figures, but they have an easy JCT because any line can intersect a polynomial only finitely many times unless it coincides with an edge.

That said, I don't think we should shy away from JCT, because it is itself an important theorem and has many many applications, like this.

 

Anyway, I was thinking of 16, the Abel-Ruffini theorem - maybe a series of formulae, where any is either a rational number, a coefficient of the polynomial, the sum, difference, product, or quotient of two previous functions, or a previous function raised to a rational power, then show that for any set of N > 5 formulae taken from such a series there must exist a polynomial of degree N whose roots don't match up?  A little worried about the "quotient" part, but I imagine any divide-by-zero error would take care of itself.

To me, Abel-Ruffini says that if we create the collection S of meromorphic functions f e. ( CC ^pm CC ) (where ( CC \ dom f ) is finite) by taking integer constant functions, the identity function, and close under sums, products, quotients where the second function is not identically zero, and n-th roots, then no function f(a) e. S satisfies f(a)^n + a f(a) + 1 = 0 for all a e. dom f, where n >= 5. (We could use a different polynomial than x^n+ax+1 if it is easier, but this is nicely concrete.) In fact, it should even be provable that f(0)^n + f(0) + 1 =/= 0 for all f in S, which is to say that x^n+x+1 has no definable roots given these building blocks.

You could be more agnostic about the parameterization of the polynomials, by trying to talk about functions f(a0,..., an) giving roots of sum_i e. (0..n) a_i x^i, but this would both make the theorem weaker and require more work to state.

Mario

--

[Thomas Brendan Leahy]

I doubt your generalization holds up - looking at the proof in J. Milne's "Fields and Galois Theory," where it's worked out as example 4.31 on page 55, I would be very surprised.

I still think starting with the general case would work better than trying to prove it immediately for any specific polynomial or family of polynomials - although harder to state, every post here seems to further establish that it'd be easier to prove.

Anyway, regarding JCT and Heron's formula - I've noticed that Jeff Hankins seems to be working toward a concept of topological boundary.  I don't want to poach, but maybe this would be a good way to define interior and exterior without JCT, and then can be used to define JCT?  That is, respectively the maximal compact open set and minimal infinite open set with the curve as a boundary, with the JCT being the existence of these sets, uniqueness (i.e., without "maximal" and "minimal"), and the impossibility of a clear path between them for Jordan curves.

[Benoit]

Anyway, regarding JCT and Heron's formula - I've noticed that Jeff Hankins seems to be working toward a concept of topological boundary.  I don't want to poach, but maybe this would be a good way to define interior and exterior without JCT, and then can be used to define JCT?  That is, respectively the maximal compact open set and minimal infinite open set with the curve as a boundary, with the JCT being the existence of these sets, uniqueness (i.e., without "maximal" and "minimal"), and the impossibility of a clear path between them for Jordan curves.

As for JCT, a detailed proof (and probably among the less difficult ones to formalize) is Thomassen's (http://www.maths.ed.ac.uk/~aar/jordan/thomass.pdf). The JCT is only the first part of the paper, so around 5 pages with all the details... but the formalization itself still looks daunting. The proof uses basic graph theory (non-planarity of K_5 and K_{3,3}). By the way, graph theory probably lends itself nicely to formalization, and could be an axis of developpement of set.mm.

--
Benoit
 

[Thierry Arnoux]

You could have a look in Mario's Mathox's ~ df-umgra to ~ konigsberg for some graph Theory in set.mm. I don't remember seeing any other.
_
Thierry

--

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 metamath+u...@googlegroups.com.

[Thomas Brendan Leahy]

Taking a trip back to sophomore year, what are we doing about 76, Fourier series?  It almost looks like it just calls for a definition, but that feels woefully inadequate - the discrete Fourier inversion theorem?

[Benoit]

For Fourier series, I would say the important result is the isomorphism of Hilbert spaces (Parseval). So a good start would be to define \ell^2(\Z) and L^2(\T).

[Glauco]

Il giorno venerdì 8 settembre 2017 10:37:25 UTC+2, Thomas Brendan Leahy ha scritto:

Taking a trip back to sophomore year, what are we doing about 76, Fourier series?  It almost looks like it just calls for a definition, but that feels woefully inadequate - the discrete Fourier inversion theorem?

I'm working on the Fourier - Dirichlet theorem (for a periodic pointwise continuous function, the Fourier Series converges to the average of the left limit and the right limit).

I'm following the proof in these notes

www2.fiu.edu/~meziani/NOTE7.pdf

(also some reference to www2.fiu.edu/~meziani/NOTE6.pdf)

I don't know how far I'll be able to go (in the worst case I'll lay down some foundation for later work).

I keep tweaking the theorem definition (having a finite left limit can be expressed in several ways. Mario's limCC is a pretty powerful tool).

The only other proof on Freek's page (in HoL Light) from the name seems to be the Cesàro summation (I guess it proves that the average of the Fourier Partial Sums converges to a given function).