Formalizing IMO B2.1972

Stanislas Polu

unread,

Feb 27, 2020, 12:08:41 PM2/27/20

to Metamath

Hi all,

I'm quite a beginner with Metamath (I have read a bunch of proofs, most of the metamath book, I have implemented my own verifier, but I haven't constructed any original proof yet) and I am looking to formalize the following proof:

IMO B2 1972: http://www.cs.ru.nl/~freek/demos/exercise/exercise.pdf
Alternative version: http://www.cs.ru.nl/~freek/demos/exercise/exercise2.pdf

(More broadly, I think this would be an interesting formalization to have in set.mm given this old but nonetheless interesting page: http://www.cs.ru.nl/~freek/demos/index.html)

I am reaching out to the community to get direction on how should I go about creating an efficient curriculum for myself in order to achieve that goal? Any other advice is obviously welcome!

Thank you!

-stan

Benoit

unread,

Feb 27, 2020, 1:27:07 PM2/27/20

to Metamath

Another proof I just found (sorry, it's not about the formalization):

Let x be such that f(x) \neq 0 and let y \in \R. Set a = g(y).

Set u_n = f(x + ny) for n \in \Z. It satisfies the linear recurrence relation u_{n+2} = 2a u_{n+1} - u_n. The characteristic relation is r^2 - 2ar + 1 = 0. The reduced discriminant is D = a^2 - 1. The sequence u_n is bounded only if D \leq 0, that is, |a| \leq 1 (recall that f(x) \neq 0 and the sequence is on \Z).

After inspection, it looks closer to Hales's solution. For formalization, the other solution looks simpler since it does not use induction. The least upper bound is defined in set.mm.

Benoît

Stanislas Polu

unread,

Feb 27, 2020, 1:42:54 PM2/27/20

to meta...@googlegroups.com

Thanks and nice!

> After inspection, it looks closer to Hales's solution. For formalization, the other solution looks simpler since it does not use induction. The least upper bound is defined in set.mm.

I have stumbled upon the supremum definition but it looks more intricate to use than a manually defining it inline on the real line (unless you’re referring to another definition of the least upper bound). That’s precisely one of the open questions I have about how to go about formalizing this type of proofs!

-stan

--
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/27635ef7-bd62-4317-a0f2-9f0873e7c499%40googlegroups.com.

Jim Kingdon

unread,

Feb 27, 2020, 1:50:41 PM2/27/20

to meta...@googlegroups.com

On February 27, 2020 8:53:29 AM PST, 'Stanislas Polu' via Metamath <meta...@googlegroups.com> wrote:
> how should I go
>about creating an efficient curriculum for myself in order to achieve
>that
>goal?

Well you'll need to study some of the existing supremum theorems: perhaps axsup and df-sup are plausible starting points.

But the other thing I'd encourage you to start with is the mechanics of writing proofs. Doesn't have to be anything new, just reproving some existing theorems could do. Example exercise: state and prove a deduction form of orel1 . You'll need to learn the proof mechanics eventually and starting in on it now will help you achieve concrete things and get a better idea for what is involved in achieving your goal.

Jon P

unread,

Feb 27, 2020, 6:19:28 PM2/27/20

to Metamath

Hi Stanislas,

Getting into metamath can be quite hard so keep asking for help if you need it, more people is always nice!

Not sure how far you have got but I suggest you get MMJ2 proof editor and then work on these problems in Filip's mathbox. Try not looking at the proofs and the producing a proof by yourself. That is a good way to start with the actual mechanics I think.

http://us.metamath.org/mpegif/mmtheorems289.html#mm28844b

Here are some tutorials for MMJ2, https://www.youtube.com/watch?v=87mnU1ckbI0&list=PL1jSu6GGefBm7RBP0Id2Sa9uyVuyhioAC

and it can be found here, http://us.metamath.org/#mmj2

Benoit

unread,

Feb 27, 2020, 7:22:29 PM2/27/20

to Metamath

I have stumbled upon the supremum definition but it looks more intricate to use than a manually defining it inline on the real line (unless you’re referring to another definition of the least upper bound). That’s precisely one of the open questions I have about how to go about formalizing this type of proofs!

I was thinking of ~suprcl and nearby theorems. For the present proof, the wanted supremum is sup ( ( abs " ( F " RR ) ) , RR , < ). But first, try to state the theorem. It should be something like

${

$d x y z t u F $. $d x y z t u G $. $d x y z t u M $. <--- probably overkill

$e |- ( ph -> F : RR --> RR ) $.

$e |- ( ph -> G : RR --> RR ) $.

$e |- ( ph -> A. x e. RR A. y e. RR .............. ) $.

$e |- ( ph -> -. A. z e. RR ( F ` z ) = 0 ) $.

$e |- ( ph -> M e. RR ) $.

$e |- ( ph -> A. t e. RR ( abs ` ( F ` t ) ) <_ M ) $.

$( B2 from IMO 1972 $)

$p |- ( ph -> A. u e. RR ( abs ` ( G ` u ) ) <_ 1 ) $= ? $.

$}

Maybe some more experienced contributors prefer another style (e.g., expressions versus functions) ?

One can also use fewer variables (e.g. replace z, t and u with x). I do not know which choice will make the proof simpler.

As suggested above, maybe start with simpler proofs for practice ?

Benoît

heiph...@wilsonb.com

unread,

Feb 27, 2020, 7:32:38 PM2/27/20

to meta...@googlegroups.com

Is it common/reasonable to write proofs directly? I am in a similar situation
as Stanislas and have proved a good handful of propositional calculus results
along with 2p2e4.

This has given me a decent handle on finding relevant theorems using metamath's
search facilities, and for the short proofs I have been working with so far,
this somewhat austere setup has been quite nice. However, with longer proofs
what problems can I expect to encounter that mmj2 and friends aim to solve?

signature.asc

Jon P

unread,

Feb 28, 2020, 10:43:31 AM2/28/20

to Metamath

Hi,

Sounds like you've made some good progress with learning the system. Here is a link to the specific place in the tutorial where David talks about the "!" feature in MMJ2 which is pretty powerful and, I think, can speed up proofs a lot.

https://youtu.be/87mnU1ckbI0?list=PL1jSu6GGefBm7RBP0Id2Sa9uyVuyhioAC&t=2634

For me personally that's the main advantage MMJ2 has.

Stanislas Polu

unread,

Feb 28, 2020, 10:45:52 AM2/28/20

to meta...@googlegroups.com

Thanks Jon,

I've installed mmj2 and went through the tutorials. Will take a look
at [0] next :+1:

[0] http://us.metamath.org/mpegif/mmtheorems289.html#mm28844b

> --
> 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.

> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/c1a31f2b-4135-45f0-b5e8-6211252593d7%40googlegroups.com.

Stanislas Polu

unread,

Feb 28, 2020, 10:50:29 AM2/28/20

to meta...@googlegroups.com

Thanks Benoit,

> I was thinking of ~suprcl and nearby theorems. For the present proof, the wanted supremum is sup ( ( abs " ( F " RR ) ) , RR , < ). But first, try to state the theorem. It should be something like
> ${
> $d x y z t u F $. $d x y z t u G $. $d x y z t u M $. <--- probably overkill
> $e |- ( ph -> F : RR --> RR ) $.
> $e |- ( ph -> G : RR --> RR ) $.
> $e |- ( ph -> A. x e. RR A. y e. RR .............. ) $.
> $e |- ( ph -> -. A. z e. RR ( F ` z ) = 0 ) $.
> $e |- ( ph -> M e. RR ) $.
> $e |- ( ph -> A. t e. RR ( abs ` ( F ` t ) ) <_ M ) $.
> $( B2 from IMO 1972 $)
> $p |- ( ph -> A. u e. RR ( abs ` ( G ` u ) ) <_ 1 ) $= ? $.
> $}

I had a similar formalization of the statement in mind. One question
for which I'm looking guidance is on using quantifiers or not.

As an example, I believe the following are all valid but presumably
drastically influence the proof strategy?

> $e |- ( ph -> -. A. z e. RR ( F ` z ) = 0 ) $.

> $e |- ( ph -> E. z e. RR ( F ` z ) =/= 0 ) $.

> $e |- ( ph -> C e. RR )
> $e |- ( 0 < ( abs ` ( F ` C ) ) ) $.

> $e |- ( ph -> C e. RR )
> $e |- ( ( F ` C ) =/= 0 ) $.

I'm very curious to better understand how do people go about making
these choices?

Best,

> --
> 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.

> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/79b726e8-f42c-452a-a6d6-95bfb11c4110%40googlegroups.com.

Thierry Arnoux

unread,

Feb 28, 2020, 11:13:50 AM2/28/20

to meta...@googlegroups.com

As an example, I believe the following are all valid but presumably
drastically influence the proof strategy?

$e |- ( ph -> -. A. z e. RR ( F ` z ) = 0 ) $.

$e |- ( ph -> E. z e. RR ( F ` z ) =/= 0 ) $.

$e |- ( ph -> C e. RR )
$e |- ( 0 < ( abs ` ( F ` C ) ) ) $.

$e |- ( ph -> C e. RR )
$e |- ( ( F ` C ) =/= 0 ) $.

I'm very curious to better understand how do people go about making
these choices?

I believe it is partly a matter of taste, and partly depends about how you plan to use the theorem. If you know you'll already have a non-zero value, then the last two versions may be of advantage.

In any case, it's actually fairly easy to swap from one formulation to the other, so they will actually not drastically impact the proof strategy.

between 1 and 2 using ~ rexnal (and df-ne)
from 4 to 2, using ~ rspcev
from 2 to 4, using ~ r19.29a for example
between 3 and 4, using ~ absgt0

In your last two formulations, however, I would have used the deduction style ( ph -> ( F ` C ) =/= 0 ) , it is weaker and therefore easier to use.
My preference usually goes to limiting the number of free variables, so I would used the last solution.

Good luck!
_
Thierry

Benoit

unread,

Feb 28, 2020, 11:17:02 AM2/28/20

to Metamath

> One question for which I'm looking guidance is on using quantifiers or not.

That's a very important question, and I hope someone with more experience will be able to shed some insight. In particular, if one has a hypothesis, say, "E. x ph", then it is common to see in textbooks things like "Let y be such that ph(y). Then [subproof], so [conclusion which does not depend on y]. Therefore, [that conclusion]." I would formalize it in set.mm by using the "deduction style" and prepending "[. y / x ]. ph" as an antecedent to each line of the subproof. Maybe there are better strategies ?

> As an example, I believe the following are all valid but presumably drastically influence the proof strategy?

> $e |- ( ph -> -. A. z e. RR ( F ` z ) = 0 ) $.

> $e |- ( ph -> E. z e. RR ( F ` z ) =/= 0 ) $.

> $e |- ( ph -> C e. RR ) $. $e |- ( 0 < ( abs ` ( F ` C ) ) ) $.
> $e |- ( ph -> C e. RR ) $. $e |- ( ( F ` C ) =/= 0 ) $.

I believe the first version (the one I used) is closest to what we mean by "F is not identically 0". The equivalence (in classical logic) with the second version is direct, using ~rexnal. I think it would be easier but "cheating" to use the third or fourth version (see above).

Benoît

Stanislas Polu

unread,

Mar 4, 2020, 8:58:24 AM3/4/20

to meta...@googlegroups.com

Hi!

I started my quest towards IMO 1972 B2 by formalizing a simple
induction problem (just for fun): `( N e. NN -> 3 || ( ( 4 ^ N ) + 5 )
)`[0] and made some good progress towards demonstrating the following
lemma:

```
imo72b2lem.1 |- ( ph -> F : RR --> RR )
imo72b2lem.2 |- ( ph -> G : RR --> RR )
imo72b2lem.3 |- ( ph -> A e. RR )
imo72b2lem.4 |- ( ph -> B e. RR )
imo72b2lem.5 |- ( ph -> ( ( F ` ( A + B ) ) +
( F ` ( A - B ) ) ) =
( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) )
imo72b2lem.6 |- ( ph -> A. x e. RR ( abs ` ( F ` x ) ) <_ 1 )

imo72b2lem |- ( ph -> ( ( abs ` ( F ` A ) ) x.
( abs ` ( G ` B ) ) )
<_ sup ( ( abs " ( F " RR ) )
, RR , < ) )
```

One thing I'm stuck on is the following: In a natural deduction
setting, how does one demonstrate an existence assuming a witness?

Basically, in order to be able to work with the `sup ( ( abs " ( F "
RR ) ) , RR , < )`, I want to go from `imo72b2lem.6` to:

```
|- ( ph -> E. c e. RR A. x e. RR ( abs ` ( F ` x ) ) <_ c )
```

From natded[1] the starting point seems to consist in applying
spesbcd[2], but I'm unclear on how to breach the difference between
`E. c ph` and `E. c e. A ph` as it does not seem to exist an
equivalent for the latter? Even assuming this problem solved, I'm also
at a loss attempting to prove the following given `imo72b2lem.6`:

```
|- ( ph -> [. 1 / c ]. A. x e. RR ( abs ` ( F ` x ) ) <_ c )
```

Thank you very much for your help on this!

-stan

[0] https://github.com/spolu/set.mm/commit/c82772aadfe13d17c722b0724526a3a72d79864c#diff-12dc1484b058d1ee6cb68a74194d66c7R641305
[1] http://us.metamath.org/mpeuni/natded.html
[2] http://us.metamath.org/mpeuni/spesbcd.html

> --
> 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.

> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/957b9c68-04bf-414b-8149-07d0801ca962%40googlegroups.com.

Benoit

unread,

Mar 4, 2020, 10:36:50 AM3/4/20

to Metamath

I started my quest towards IMO 1972 B2 by formalizing a simple
induction problem (just for fun): `( N e. NN -> 3 || ( ( 4 ^ N ) + 5 )

I think ~ inductionexd (with the caveat below) is a nice instructive example, and could be moved to main, as the first theorem of the new subsection

17.1.5 Examples of proofs by induction

Do the maintainers agree ? Which labeling ? ~ ex-induction0 ?

Beware that in set.mm, the symbol NN does not denote the natural numbers, but only the nonzero natural numbers. Therefore, stating ~ inductionexd with " N e. NN0 " is more... natural. (And its proof might be shorter since the base case involves smaller numbers.)

I hope you do a PR with your mathbox. Your eqdivs2d, leeqd and leeq2d seem to be special cases of oveq2. They are probably not worth stating. In comments, use " ~ label " to link to other statements. Use "MM-PA>minimize *" after completing your proofs (maybe you do it already; and more generally, https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md).

One thing I'm stuck on is the following: In a natural deduction
setting, how does one demonstrate an existence assuming a witness?

From natded[1] the starting point seems to consist in applying
spesbcd[2], but I'm unclear on how to breach the difference between
`E. c ph` and `E. c e. A ph` as it does not seem to exist an
equivalent for the latter?

There should be a theorem in set.mm of the form
${

$d x B $.

rspesbcd.1 $e |- ( ph -> A e. B ) $.
rspesbcd.2 $e |- ( ph -> [. A / x ]. ps ) $.
rspesbcd $p |- ( ph -> E. x e. B ps ) $= ? $.

$}
If not, add it: just use spesbcd with the formula "( x e. B /\ ps )".

Even assuming this problem solved, I'm also
at a loss attempting to prove the following given `imo72b2lem.6`:

```
|- ( ph -> [. 1 / c ]. A. x e. RR ( abs ` ( F ` x ) ) <_ c )
```

This would be a long but automatic derivation. I think mmj2 does this kind of things automatically. But why would you need this ?

Benoît

Stanislas Polu

unread,

Mar 4, 2020, 11:09:56 AM3/4/20

to meta...@googlegroups.com

Thanks Benoit for the comments on my current branch. I will definitely apply them and submit my mathbox to set.mm!

> This would be a long but automatic derivation. I think mmj2 does this kind of things automatically. But why would you need this ?

Wouldn't I need this to go from the substituted rspesbcd.2 (following your naming convention):

|- ( ph -> [. 1 / x ]. A. x e. RR ( abs ` ( F ` x ) ) <_ 1 )

to the hypothesis imo72b2lem.6 (following my naming convention):

|- ( ph -> A. x e. RR ( abs ` ( F ` x ) ) <_ 1 )

Maybe I'm missing something but my high level goal is to prove:

|- ( ph -> E. c e. RR A. x e. RR ( abs ` ( F ` x ) ) <_ c )

using:

|- ( ph -> A. x e. RR ( abs ` ( F ` x ) ) <_ 1 )

Thanks!

-stan

--

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/99e1a2bd-d406-44ee-a2ef-8fd9739d2df4%40googlegroups.com.

Jim Kingdon

unread,

Mar 4, 2020, 11:34:35 AM3/4/20

to 'Stanislas Polu' via Metamath

On March 4, 2020 5:58:12 AM PST, 'Stanislas Polu' via Metamath <meta...@googlegroups.com> wrote:

> the starting point seems to consist in applying
>spesbcd[2], but I'm unclear on how to breach the difference between
>`E. c ph` and `E. c e. A ph` as it does not seem to exist an
>equivalent for the latter?

The direct answer to this question would appear to be http://us.metamath.org/mpeuni/rspsbc.html

There are usually a lot of ways to arrange this kind of logic though, and often the theorems using implicit substitution are easier to use, perhaps something like http://us.metamath.org/mpeuni/rspcev.html

Hope that isn't too bewildering. To get started it is more important to find one way that works, and worry about all the variations later (or let the minimizer worry about them).

Thierry Arnoux

unread,

Mar 4, 2020, 11:46:15 AM3/4/20

to meta...@googlegroups.com, Jim Kingdon

> Maybe I'm missing something but my high level goal is to prove:
>

> |- ( ph -> E. c e. RR A. x e. RR ( abs ` ( F ` x ) ) <_ c )
>

> using:

>
> |- ( ph -> A. x e. RR ( abs ` ( F ` x ) ) <_ 1 )

As pointed by Jim, the easier way to do this is to use ~rspcev and avoid
the explicit substitution. You will need to prove:

|- ( c = 1 -> ( A. x e. RR ( abs ` ( F ` x ) ) <_ c <-> A. x e. RR ( abs
` ( F ` x ) ) <_ 1 ) )

In my case, MMJ2 often automatically fills in ~cbvral, but the right
theorem for that step is ~ralbidv.

Stanislas Polu

unread,

Mar 4, 2020, 12:28:55 PM3/4/20

to meta...@googlegroups.com, Jim Kingdon

Thanks!

I was able to reach my objective using the rspcedvd variant (shouldn't
it be referenced from natded?), closer to my current proof setup \o/

```
d994::1red |- ( ph -> 1 e. RR )
d997::simpr |- ( ( ph /\ c = 1 ) -> c = 1 )
d998:d997:breq2d |- ( ( ph /\ c = 1 )
-> ( ( abs ` ( F ` x ) ) <_ c
<-> ( abs ` ( F ` x ) ) <_ 1 ) )
d995:d998:ralbidv |- ( ( ph /\ c = 1 )

-> ( A. x
e. RR
( abs ` ( F ` x ) ) <_ c
<-> A. x e. RR ( abs ` ( F ` x ) ) <_ 1 ) )

exsup1:d994,d995,6:rspcedvd |- ( ph -> E. c e. RR A. x e. RR ( abs ` ( F ` x ) ) <_ c )
```

-stan

--
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.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e5d2f406-8edd-75fa-0fd9-9440affad7ab%40gmx.net.

Benoit

unread,

Mar 4, 2020, 12:29:13 PM3/4/20

to Metamath

Stan: you're right about the need to prove this (if using explicit substitution): look for the utility theorems exchanging [. / ]. with other symbols (quantifiers, operations). As said by Jim and Thierry, who are more experienced in proof building, implicit substitution might be easier to use. I think it is instructive to compare the details of both proving styles on a specific example (e.g. ralbidv, suggested by Thierry, would be analogous to exchanging [. / ]. with A.).

Still, I think adding what I called rspesbcd could prove useful (if it is not already in set.mm under another label; I cannot search now, but it probably is already somewhere).

Benoît

Norman Megill

unread,

Mar 4, 2020, 2:09:06 PM3/4/20

to Metamath

On Wednesday, March 4, 2020 at 10:36:50 AM UTC-5, Benoit wrote:

...

Beware that in set.mm, the symbol NN does not denote the natural numbers, but only the nonzero natural numbers. Therefore, stating ~ inductionexd with " N e. NN0 " is more... natural. (And its proof might be shorter since the base case involves smaller numbers.)

..

This should probably be another thread, but maybe it is time to rename "NN" to "NN1" to put this issue (which has been discussed before) to rest. As I've made known, I personally prefer NN since it is the set of "natural numbers" that books on analysis usually use, and analysis is all about the real and complex numbers that NN is a subset of. But I recognize that at some point avoiding confusion may become more important than aesthetics or conforming to literature practice.

In the meantime, note that we changed most comments in set.mm to use "positive integer" instead of "natural number" for NN members to avoid ambiguity, so that is one way to tell what NN means if you forget.

In early set.mm, we do call members of _om (omega), which start at zero, "natural numbers" in comments, because that is the practice of set theorists (and it would be rather hard to develop ordinals without zero). Interestingly, zero becomes inconvenient and isn't used for the Dedekind construction of reals, so we define positive ordinals with ~ df-ni (intended to be used only for the construction).

Norm

Stanislas Polu

unread,

Mar 4, 2020, 2:30:17 PM3/4/20

to meta...@googlegroups.com

I'm now looking to prove that `( abs " ( F " RR ) ) =/= (/)` given `F : RR --> RR`. From my exploration of the definition of --> I believe this should be enough but I don't see an easy path towards that? Would anybody have an example in mind that could give me a little bit of inspiration?

Thanks for the continued support!

-stan

--

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/ebdd296f-6bcd-49e0-88c8-c7fef3628cdd%40googlegroups.com.

Mario Carneiro

unread,

Mar 4, 2020, 2:45:24 PM3/4/20

to metamath

Can't look right now, but you should search for a theorem of the form A = (/) <-> ( F " A ) = (/) .

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACZd_0zFiVT5n-7%2BYh-YL2mDCLMom6R66gq7gbMT7tgJzTzadQ%40mail.gmail.com.

fl

unread,

Mar 4, 2020, 3:47:38 PM3/4/20

to Metamath

This should probably be another thread, but maybe it is time to rename "NN" to "NN1" to put this issue (which has been discussed before) to rest.

I approve. Thank you. Thank you. Thank you. Thank you.

Positive number is not unambiguous. For some people 0 is a positive number.

--

FL

Stanislas Polu

unread,

Mar 5, 2020, 11:07:44 AM3/5/20

to meta...@googlegroups.com

Thanks Mario!

I just finished formalizing the following lemma (which is a good chunk of the proof \o/):

```
$d F c x $. $d c ph x $.
imo72b2lem.1 $e |- ( ph -> F : RR --> RR ) $.
imo72b2lem.2 $e |- ( ph -> G : RR --> RR ) $.
imo72b2lem.3 $e |- ( ph -> A e. RR ) $.
imo72b2lem.4 $e |- ( ph -> B e. RR ) $.
imo72b2lem.5 $e |- ( ph -> ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) = ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) ) $.
imo72b2lem.6 $e |- ( ph -> A. x e. ( abs " ( F " RR ) ) x <_ 1 ) $.
imo72b2lem.7 $e |- ( ph -> E. x e. RR ( F ` x ) =/= 0 ) $.

imo72b2lem $p |- ( ph -> ( ( abs ` ( F ` A ) ) x. ( abs ` ( G ` B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) ) $=
```

Proof here: https://github.com/spolu/set.mm/commit/454132a35254c17c4e54353b5c2c772eeb2ebb65

One thing I'm quite dissatisfied with is the shape of `imo72b2lem.6`. I'd much rather have the more natural/intuitive expression `|- ( ph -> A. x e. RR ( abs ` ( F `x ) ) <_ 1 )` but I completely failed to prove imo72b2lem.6 from it. Any help on this would be greatly appreciated!

-stan

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStosWZ0BEO7zjpeW90VMNT3pf-Kr6nUaqLefJyA%3Dgwa2Q%40mail.gmail.com.

Mario Carneiro

unread,

Mar 5, 2020, 12:27:25 PM3/5/20

to metamath

There is a theorem specifically for that translation, something like A. x e. ( F " A ) P[x] <-> A. y e. A P[( F ` y )]. It's probably called ralima but you've caught me on the bus again.

Mario

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACZd_0zgFkBD0kOaAXNGyB3PL18Qt06uSHV%3DEmwOjh6Rk5j3OQ%40mail.gmail.com.

Stanislas Polu

unread,

Mar 6, 2020, 11:02:57 AM3/6/20

to meta...@googlegroups.com

Thanks again Mario!

I made more progress towards the final demonstration of the full IMO problem. Working on the following lemma:

```
h1::imo72b2lem1.1 |- ( ph -> F : RR --> RR )
h2::imo72b2lem1.7 |- ( ph -> E. x e. RR ( F ` x ) =/= 0 )
h3::imo72b2lem0.6 |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 )

```

I need to prove the following goal which seems pretty obvious but I'm struggling to find a way to discharge it:

```
d84:: |- ( ( ph /\ x e. RR ) -> ( ( abs o. F ) ` x ) =/= (/) )
```

Any idea on how to proceed with this?

Thanks thanks!

-stan

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSs4iVxdk7Uz1_bW-heUVCJy-CMGENLNtzWd8%2B12rFEVBQ%40mail.gmail.com.

Mario Carneiro

unread,

Mar 6, 2020, 5:58:14 PM3/6/20

to metamath

The composition function value combination is easy enough to eliminate using fvco, but the equality to the empty set is a type error, because the lhs is a real number and the question of whether the empty set is a real number is deliberately left ambiguous by the real number axioms. So I would like to know what steps got you to this point. There are some function value theorems that assume this as a "convenience" but there should be analogues of them that don't (probably with some other assumption like the function is a set).

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACZd_0x2N3k16mC%2Byc_%3D6HvNQ3OWpAXtQ3fHkMv%3DPqERwFR60Q%40mail.gmail.com.

Stanislas Polu

unread,

Mar 7, 2020, 2:54:34 AM3/7/20

to meta...@googlegroups.com

Interesting!

It basically comes from an attempt at satisfying the conditions for eliman0. Here's the full proof draft:

```

$( <MM> <PROOF_ASST> THEOREM=imo72b2lem1 LOC_AFTER=?

h1::imo72b2lem1.1 |- ( ph -> F : RR --> RR )
h2::imo72b2lem1.7 |- ( ph -> E. x e. RR ( F ` x ) =/= 0 )
h3::imo72b2lem0.6 |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 )

!d84:: |- ( ( ph /\ x e. RR ) -> ( ( abs o. F ) ` x ) =/= (/) )
d83:d84:adantrr |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( ( abs o. F ) ` x ) =/= (/) )
d81:d83:neneqd |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> -. ( ( abs o. F ) ` x ) = (/) )

d95:1:ffvelrnda |- ( ( ph /\ x e. RR ) -> ( F ` x ) e. RR )
d94:d95:adantrr |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( F ` x ) e. RR )
d92:d94:recnd |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( F ` x ) e. CC )
d93::simprr |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( F ` x ) =/= 0 )
d91:d92,d93:absrpcld |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( abs ` ( F ` x ) ) e. RR+ )
d9:d91:rpgt0d |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> 0 < ( abs ` ( F ` x ) ) )

d80::simprl |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> x e. RR )
d82::eliman0 |- ( ( x e. RR /\ -. ( ( abs o. F ) ` x ) = (/) ) -> ( ( abs o. F ) ` x ) e. ( ( abs o. F ) " RR ) )
d75:d80,d81,d82:syl2anc |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( ( abs o. F ) ` x ) e. ( ( abs o. F ) " RR ) )
oeqaa::imaco |- ( ( abs o. F ) " RR ) = ( abs " ( F " RR ) )
d71:d75,oeqaa:syl6eleq |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( ( abs o. F ) ` x ) e. ( abs " ( F " RR ) ) )
d73:1:adantr |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> F : RR --> RR )
d74::simprl |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> x e. RR )
d72:d73,d74:fvco3d |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( ( abs o. F ) ` x ) = ( abs ` ( F ` x ) ) )
d7:d72,d71:eqeltrrd |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( abs ` ( F ` x ) ) e. ( abs " ( F " RR ) ) )

d10::simpr |- ( ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) /\ z = ( abs ` ( F ` x ) ) ) -> z = ( abs ` ( F ` x ) ) )
d8:d10:breq2d |- ( ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) /\ z = ( abs ` ( F ` x ) ) ) -> ( 0 < z <-> 0 < ( abs ` ( F ` x ) ) ) )

d6:d7,d8,d9:rspcedvd |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> E. z e. ( abs " ( F " RR ) ) 0 < z )
qed:2,d6:rexlimddv |- ( ph -> E. z e. ( abs " ( F " RR ) ) 0 < z )

$)

-stan

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSv0pGnDb%2Bfae5_ZS_mAK_R6MeMQPAL4gsHD-9S5g2XSVQ%40mail.gmail.com.

Stanislas Polu

unread,

Mar 7, 2020, 2:59:48 AM3/7/20

to meta...@googlegroups.com

(fvco3d is a natural deduction form of fvco3 proved here: https://github.com/metamath/set.mm/commit/454132a35254c17c4e54353b5c2c772eeb2ebb65#diff-12dc1484b058d1ee6cb68a74194d66c7R641421-R641429)

-stan

Mario Carneiro

unread,

Mar 7, 2020, 4:47:33 AM3/7/20

to metamath

Yep, you correctly identified eliman0 as the bad lemma here. I hadn't heard of it but it's using a trick to avoid having to prove that the input is in the domain of the function. Using metamath.exe, I searched for this pattern and got a few results:

MM> sea * '( ? ` ? ) e. ( ? " ? )'/j
19563 eliman0 $p |- ( ( A e. B /\ -. ( F ` A ) = (/) ) -> ( F ` A ) e. ( F " B
) )
20603 funfvima $p |- ( ( Fun F /\ B e. dom F ) -> ( B e. A -> ( F ` B ) e. ( F
" A ) ) )
20604 funfvima2 $p |- ( ( Fun F /\ A C_ dom F ) -> ( B e. A -> ( F ` B ) e. ( F
" A ) ) )
20611 fnfvima $p |- ( ( F Fn A /\ S C_ A /\ X e. S ) -> ( F ` X ) e. ( F " S )
)
20740 f1elima $p |- ( ( F : A -1-1-> B /\ X e. A /\ Y C_ A ) -> ( ( F ` X ) e.
( F " Y ) <-> X e. Y ) )
79323 kqfvima $e |- F = ( x e. X |-> { y e. J | x e. y } ) $p |- ( ( J e. (
TopOn ` X ) /\ U e. J /\ A e. X ) -> ( A e. U <-> ( F ` A ) e. ( F " U ) )
)

and the actual theorems you want to reference are either funfvima, funfvima2, or fnfvima depending on how the function is presented. (Arguably eliman0 should be moved to after fnfvima and given a more similar name, e.g. fviman0.) In this case, the function has known domain and range so I would go for fnfvima, using fnco to prove that ( abs o. F ) Fn RR.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACZd_0yzRWT%3DZn6qPpgXPbzSabuOqHVSLW6uG9aF6S6yYht5mA%40mail.gmail.com.

Stanislas Polu

unread,

Mar 7, 2020, 7:25:44 AM3/7/20

to meta...@googlegroups.com

Thanks! Makes perfect sense. I will adapt the proof accordingly!

-stan

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSutmF6LrPLUHM%3DoBbd5d_4kE8jeM9j-gFsc9tnYVU4Mcg%40mail.gmail.com.

Stanislas Polu

unread,

Mar 9, 2020, 8:41:28 AM3/9/20

to meta...@googlegroups.com

Finished proof available here: https://github.com/metamath/set.mm/compare/develop...spolu:spolu-mathbox?expand=1

What an adventure, thank you all for your precious help!

```

$d B c t $. $d B u v $. $d B x $. $d B t y $. $d F c t $. $d F u v $.
$d F x $. $d F t y $. $d G c t $. $d G u v $. $d G x $. $d G t y $.
$d c ph t $. $d ph u v $. $d ph x $. $d ph t y $. $d u y $.
imo72b2.1 $e |- ( ph -> F : RR --> RR ) $.
imo72b2.2 $e |- ( ph -> G : RR --> RR ) $.
imo72b2.4 $e |- ( ph -> B e. RR ) $.
imo72b2.5 $e |- ( ph -> A. u e. RR A. v e. RR ( ( F ` ( u + v ) ) + ( F ` ( u - v ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` v ) ) ) ) $.
imo72b2.6 $e |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 ) $.
imo72b2.7 $e |- ( ph -> E. x e. RR ( F ` x ) =/= 0 ) $.
$( IMO 1972 B2. $)
imo72b2 $p |- ( ph -> ( abs ` ( G ` B ) ) <_ 1 ) $=

```

One question that remains pertains to DVs: I'm surprised to see the DVs bubble up even if the variable does not appear in the final statement? Why is that the case?

Also, to answer my own question as well as react on Benoit's remark:

> > One question for which I'm looking guidance is on using quantifiers or not.

> That's a very important question, and I hope someone with more experience will be able to shed some insight. In particular, if one has a hypothesis, say, "E. x ph", then it is common to see in textbooks things like "Let y be such that ph(y). Then [subproof], so [conclusion which does not depend on y]. Therefore, [that conclusion]." I would formalize it in set.mm by using the "deduction style" and prepending "[. y / x ]. ph" as an antecedent to each line of the subproof. Maybe there are better strategies ?

From the experience formalizing imo72b2, I think that when relying on natural deduction forms, hypotheses should favor quantifiers (stronger) while conclusions shouldn't (easier to work with). Going from a lemma without quantifier to a resolved goal with quantifier is relatively easy with rspcdv, rspcedvd and the likes.

-stan

Jon P

unread,

Mar 9, 2020, 10:25:03 AM3/9/20

to Metamath

Congratulations on finishing your proof!

Stanislas Polu

unread,

Mar 9, 2020, 10:54:51 AM3/9/20

to meta...@googlegroups.com

Thanks! Submitted a PR here: https://github.com/metamath/set.mm/pull/1522

Interesting side-note: I calculated the "de Bruijn factor" as defined/reported in [0][1] and got ~12 (from the set.mm format) and ~15 (from the .mmp formats). Far above the other systems reported in [0] but not as high as I would have anticipated.

-stan

[0] http://www.cs.ru.nl/~freek/factor/
[1] http://www.cs.ru.nl/~freek/demos/index.html

On Mon, Mar 9, 2020 at 3:25 PM Jon P <drjonp...@gmail.com> wrote:

Congratulations on finishing your proof!

--

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/de4a6e40-9ff7-4a50-840e-42db0490bee4%40googlegroups.com.

Stanislas Polu

unread,

Mar 12, 2020, 3:50:17 AM3/12/20

to meta...@googlegroups.com

Wanted to follow-up on the question above that may have been lost in translation, if anyone could shed some light on it:

> One question that remains pertains to DVs: I'm surprised to see the DVs bubble up even if the variable does not appear in the final statement? Why is that the case?

Thanks!

-stan

Mario Carneiro

unread,

Mar 12, 2020, 5:20:57 AM3/12/20

to metamath

This is a minor design decision in the metamath spec. It's nice to be explicit about this, but you can always safely assume that all dummy variables are disjoint from all other variables with no loss in the generality of the theorem, and some verifiers even do this automatically. But the spec itself requires that these annotations be present, so that would not be strictly conforming.

Mario

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACZd_0wpSzR5JhXYHkGLSq9F%2ByUVc_p-JAZ%2BnX5gO26gKsz82A%40mail.gmail.com.

Stanislas Polu

unread,

Mar 12, 2020, 5:51:41 AM3/12/20

to meta...@googlegroups.com

Thanks! Very clear.

I was first worried about having misunderstood something fundamental about DVs (thanks for clarifying) and secondly about exhaustion of variable names which somewhat hurts the user experience but I presume it's a minor point.

-stan

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStM%2BGKK%3DpcBdeyNUr9pUe78pbNsdeeuu7jL8vLtTUMEaA%40mail.gmail.com.

Mario Carneiro

unread,

Mar 12, 2020, 6:14:42 AM3/12/20

to metamath

Exhaustion of variable names is a sort of theoretical concern, because "26 variables should be enough for anyone". In practice it usually just means that you can't be particularly descriptive with your variable naming. For automated theorem generation, I usually just make up $v/$f statements on the spot, so you obtain infinite variables that way. But set.mm mostly just sticks to its original alphabet set. Class variables are the most common, and those have a few more than 26 because of symbol variables like .+ that give you a bit more symbolic flexibility, while wff variables have a lot less than 26 because we don't have the whole greek alphabet, I think there is only 12 or so and I'm actually using the whole set in simp-11l. Generally speaking, if you need that many variables you probably should break your theorem down into more intelligible pieces and/or make more definitions, which can be used to encapsulate binders and free up some more variables for use.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACZd_0zcyMSuAzFfhbEJCNp1WJwpWVE6_%3DkowJ6zrW5u%2BfYqSg%40mail.gmail.com.

Marnix Klooster

unread,

Mar 23, 2020, 1:38:54 PM3/23/20

to Metamath

Hi Stan,

If I were to formalize this in Metamath, I'd use the first proof, but in a more calculational format.

I've attached it, unfortunately as a picture.

Yes, this is a longer proof, but it seems somehow easier to me.

Hope this helps someone... :-)

Groetjes,

<><

Marnix

Op do 27 feb. 2020 om 18:08 schreef 'Stanislas Polu' via Metamath <meta...@googlegroups.com>:

Hi all,

I'm quite a beginner with Metamath (I have read a bunch of proofs, most of the metamath book, I have implemented my own verifier, but I haven't constructed any original proof yet) and I am looking to formalize the following proof:

IMO B2 1972: http://www.cs.ru.nl/~freek/demos/exercise/exercise.pdf
Alternative version: http://www.cs.ru.nl/~freek/demos/exercise/exercise2.pdf

(More broadly, I think this would be an interesting formalization to have in set.mm given this old but nonetheless interesting page: http://www.cs.ru.nl/~freek/demos/index.html)

I am reaching out to the community to get direction on how should I go about creating an efficient curriculum for myself in order to achieve that goal? Any other advice is obviously welcome!

Thank you!

-stan

--
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.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/78223c8d-eddf-4f84-970d-6b0cbb20dab9%40googlegroups.com.

--

Marnix Klooster
marnix....@gmail.com

Stanislas Polu

unread,

Mar 23, 2020, 4:05:32 PM3/23/20

to meta...@googlegroups.com

Hi Marnix!

Thanks for sharing. The proof I formalized[0] is very closed but I agree is also a bit more complicated.

Out of curiosity, where did you find that proof which has a very "formal" presentation?

Best,

-stan

[0] http://us.metamath.org/mpeuni/imo72b2.html

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAF7V2P-2gAJsLSmnz-AtneyXNOGmG5w%3Dcn2gYVXk94FUQ5XdPg%40mail.gmail.com.

Marnix Klooster

unread,

Mar 24, 2020, 4:00:28 AM3/24/20

to Metamath

Hi Stan,

I designed and wrote that proof myself. :-) This is the style designed and advocated by Edsger W. Dijkstra and this collaborators. See his EWD1300 for an overview and his reasoning.

So what I like about this proof and this style, is several things, like avoiding rabbits-out-of-hats and instead trying to provide insight: "why would one think about taking a least upper bound here?"; preferring a direct style instead of resorting to contradiction; making explicit which assumptions are used where; making the proof easier on the reader so that they don't have to guess why a certain step is correct; and this style of proof is (at least for me) easier to reinvent later: just go through the same heuristics again and most of the proof writes itself.

For example, the original proof starts with the rabbit 2k (so 2 sup |f(z)|) and then makes that expression more complex. The simple act of inverting the order of that calculation makes the proof easier to understand, at least for me, but I think for many other readers as well.

And it makes proofs easier to formalize, I think.

-Marnix

Op ma 23 mrt. 2020 om 21:05 schreef 'Stanislas Polu' via Metamath <meta...@googlegroups.com>:

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACZd_0x56Ck-geksHLs0pRZwCLb_oaisqxyFpH4Ds5haXkrU9Q%40mail.gmail.com.

--

Marnix Klooster
marnix....@gmail.com

Stanislas Polu

unread,

Mar 24, 2020, 4:34:32 AM3/24/20

to meta...@googlegroups.com

Very nice. Seems definitely beneficial to prepare a proof for formalization.

-stan

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAF7V2P8PEpV8dy-dkmcVaUo9CAZAi1iMw41%2BXsa-K07Lyi2D7g%40mail.gmail.com.

Dirk-Anton Broersen

unread,

Mar 24, 2020, 9:09:53 AM3/24/20

to meta...@googlegroups.com, Dirk-Anton Broersen

I'm also a beginner. And I received this email. I posted lately an email about a finding. I don 't know of it's unique or known or if it has resemblance.

It's also about triangelar numbers in a formula.

E

x = x + 1

(triangelar number) power 2 / x

triangelar number = triangelar number + triangelar number + 1

First results are and I also wrote a programm in c++ wich you can copy paste to cpp.sh to see the results.

1 1 (1/1) 1 = 1 ^2

2 4.5 (9/2) 9 = 3 ^2

3 12 (36/3) 36 = 6 ^2

4 25 (100/4) 100 = 10 ^2

1 <==> 4.5 <==> 12 <==> 25 <==> ..

within these gaps there is an amount of primenumbers that inscrease. Percentual it's also intersting.

I'll send next the first number of results of the programm. then it's also clear what number of primes are increasing.

Including the programm.

I don 't wanna frustrate others work. This might be seen as trolling. I just received this email, but I tought this might be something. I'm an undergraduated mathematician. And it has also to do with triangelar numbers.

With friendly regards,

Dirk-Anton Broersen

Outlook for Android downloaden

From: 'Stanislas Polu' via Metamath <meta...@googlegroups.com>
Sent: Monday, March 23, 2020 9:05:17 PM
To: meta...@googlegroups.com <meta...@googlegroups.com>
Subject: Re: [Metamath] Formalizing IMO B2.1972

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACZd_0x56Ck-geksHLs0pRZwCLb_oaisqxyFpH4Ds5haXkrU9Q%40mail.gmail.com.

Dirk-Anton Broersen

unread,

Mar 24, 2020, 9:09:53 AM3/24/20

to metamath@googlegroups.com <metamath@googlegroups.com>, Dirk-Anton Broersen

According to last mail,

Some results (130)

1: 1 0 <=> 1 1 per gap=> 100 % total=> 50 %

2: 2 1 <=> 4.5 1 per gap=> 57.1429 % total=> 85.7143 %

3: 3 4.5 <=> 12 1 per gap=> 40 % total=> 52.8571 %

4: 4 12 <=> 25 1 per gap=> 30.7692 % total=> 38.1538 %

5: 5 25 <=> 45 1 per gap=> 25 % total=> 29.8077 %

6: 7 45 <=> 73.5 1.16667 per gap=> 24.5614 % total=> 24.9373 %

7: 9 73.5 <=> 112 1.28571 per gap=> 23.3766 % total=> 24.4133 %

8: 8 112 <=> 162 1 per gap=> 16 % total=> 22.557 %

9: 11 162 <=> 225 1.22222 per gap=> 17.4603 % total=> 16.146 %

10: 14 225 <=> 302.5 1.4 per gap=> 18.0645 % total=> 17.5152 %

11: 15 302.5 <=> 396 1.36364 per gap=> 16.0428 % total=> 17.896 %

12: 19 396 <=> 507 1.58333 per gap=> 17.1171 % total=> 16.1254 %

13: 19 507 <=> 637 1.46154 per gap=> 14.6154 % total=> 16.9384 %

14: 23 637 <=> 787.5 1.64286 per gap=> 15.2824 % total=> 14.6599 %

15: 25 787.5 <=> 960 1.66667 per gap=> 14.4928 % total=> 15.233 %

16: 29 960 <=> 1156 1.8125 per gap=> 14.7959 % total=> 14.5106 %

17: 29 1156 <=> 1377 1.70588 per gap=> 13.1222 % total=> 14.7029 %

18: 37 1377 <=> 1624.5 2.05556 per gap=> 14.9495 % total=> 13.2183 %

19: 33 1624.5 <=> 1900 1.73684 per gap=> 11.9782 % total=> 14.8009 %

20: 38 1900 <=> 2205 1.9 per gap=> 12.459 % total=> 12.0011 %

21: 43 2205 <=> 2541 2.04762 per gap=> 12.7976 % total=> 12.4744 %

22: 50 2541 <=> 2909.5 2.27273 per gap=> 13.5685 % total=> 12.8311 %

23: 45 2909.5 <=> 3312 1.95652 per gap=> 11.1801 % total=> 13.469 %

24: 57 3312 <=> 3750 2.375 per gap=> 13.0137 % total=> 11.2535 %

25: 56 3750 <=> 4225 2.24 per gap=> 11.7895 % total=> 12.9666 %

26: 61 4225 <=> 4738.5 2.34615 per gap=> 11.8793 % total=> 11.7928 %

27: 62 4738.5 <=> 5292 2.2963 per gap=> 11.2014 % total=> 11.8551 %

28: 74 5292 <=> 5887 2.64286 per gap=> 12.437 % total=> 11.244 %

29: 68 5887 <=> 6525 2.34483 per gap=> 10.6583 % total=> 12.3777 %

30: 77 6525 <=> 7207.5 2.56667 per gap=> 11.2821 % total=> 10.6784 %

31: 83 7207.5 <=> 7936 2.67742 per gap=> 11.3933 % total=> 11.2855 %

32: 83 7936 <=> 8712 2.59375 per gap=> 10.6959 % total=> 11.3721 %

33: 95 8712 <=> 9537 2.87879 per gap=> 11.5152 % total=> 10.72 %

34: 94 9537 <=> 10412.5 2.76471 per gap=> 10.7367 % total=> 11.4929 %

35: 96 10412.5 <=> 11340 2.74286 per gap=> 10.3504 % total=> 10.726 %

36: 101 11340 <=> 12321 2.80556 per gap=> 10.2956 % total=> 10.3489 %

37: 114 12321 <=> 13357 3.08108 per gap=> 11.0039 % total=> 10.3143 %

38: 110 13357 <=> 14449.5 2.89474 per gap=> 10.0686 % total=> 10.9799 %

39: 124 14449.5 <=> 15600 3.17949 per gap=> 10.7779 % total=> 10.0864 %

40: 121 15600 <=> 16810 3.025 per gap=> 10 % total=> 10.7589 %

41: 133 16810 <=> 18081 3.2439 per gap=> 10.4642 % total=> 10.0111 %

42: 125 18081 <=> 19414.5 2.97619 per gap=> 9.37383 % total=> 10.4388 %

43: 147 19414.5 <=> 20812 3.4186 per gap=> 10.5188 % total=> 9.39985 %

44: 150 20812 <=> 22275 3.40909 per gap=> 10.2529 % total=> 10.5129 %

45: 153 22275 <=> 23805 3.4 per gap=> 10 % total=> 10.2474 %

46: 153 23805 <=> 25403.5 3.32609 per gap=> 9.57147 % total=> 9.99088 %

47: 168 25403.5 <=> 27072 3.57447 per gap=> 10.0689 % total=> 9.58184 %

48: 169 27072 <=> 28812 3.52083 per gap=> 9.71264 % total=> 10.0617 %

49: 165 28812 <=> 30625 3.36735 per gap=> 9.10094 % total=> 9.70041 %

50: 187 30625 <=> 32512.5 3.74 per gap=> 9.90728 % total=> 9.11675 %

51: 193 32512.5 <=> 34476 3.78431 per gap=> 9.82939 % total=> 9.90579 %

52: 188 34476 <=> 36517 3.61538 per gap=> 9.21117 % total=> 9.81772 %

53: 199 36517 <=> 38637 3.75472 per gap=> 9.38679 % total=> 9.21442 %

54: 206 38637 <=> 40837.5 3.81481 per gap=> 9.36151 % total=> 9.38633 %

55: 230 40837.5 <=> 43120 4.18182 per gap=> 10.0767 % total=> 9.37428 %

56: 210 43120 <=> 45486 3.75 per gap=> 8.87574 % total=> 10.0556 %

57: 224 45486 <=> 47937 3.92982 per gap=> 9.13913 % total=> 8.88028 %

58: 239 47937 <=> 50474.5 4.12069 per gap=> 9.41872 % total=> 9.14387 %

59: 239 50474.5 <=> 53100 4.05085 per gap=> 9.10303 % total=> 9.41346 %

60: 246 53100 <=> 55815 4.1 per gap=> 9.06077 % total=> 9.10234 %

61: 269 55815 <=> 58621 4.40984 per gap=> 9.5866 % total=> 9.06925 %

62: 257 58621 <=> 61519.5 4.14516 per gap=> 8.86666 % total=> 9.57517 %

63: 265 61519.5 <=> 64512 4.20635 per gap=> 8.85547 % total=> 8.86648 %

64: 282 64512 <=> 67600 4.40625 per gap=> 9.13212 % total=> 8.85973 %

65: 274 67600 <=> 70785 4.21538 per gap=> 8.60283 % total=> 9.1241 %

66: 297 70785 <=> 74068.5 4.5 per gap=> 9.04523 % total=> 8.60943 %

67: 302 74068.5 <=> 77452 4.50746 per gap=> 8.92567 % total=> 9.04347 %

68: 314 77452 <=> 80937 4.61765 per gap=> 9.01004 % total=> 8.92689 %

69: 319 80937 <=> 84525 4.62319 per gap=> 8.89075 % total=> 9.00834 %

70: 315 84525 <=> 88217.5 4.5 per gap=> 8.53081 % total=> 8.88568 %

71: 333 88217.5 <=> 92016 4.69014 per gap=> 8.76662 % total=> 8.53408 %

72: 355 92016 <=> 95922 4.93056 per gap=> 9.08858 % total=> 8.77103 %

73: 344 95922 <=> 99937 4.71233 per gap=> 8.56787 % total=> 9.08155 %

74: 352 99937 <=> 104062 4.75676 per gap=> 8.5323 % total=> 8.5674 %

75: 364 104062 <=> 108300 4.85333 per gap=> 8.58997 % total=> 8.53306 %

76: 371 108300 <=> 112651 4.88158 per gap=> 8.52678 % total=> 8.58915 %

77: 379 112651 <=> 117117 4.92208 per gap=> 8.48634 % total=> 8.52626 %

78: 400 117117 <=> 121700 5.12821 per gap=> 8.72886 % total=> 8.48941 %

79: 400 121700 <=> 126400 5.06329 per gap=> 8.50973 % total=> 8.72612 %

80: 406 126400 <=> 131220 5.075 per gap=> 8.42324 % total=> 8.50867 %

81: 417 131220 <=> 136161 5.14815 per gap=> 8.43959 % total=> 8.42344 %

82: 438 136161 <=> 141224 5.34146 per gap=> 8.65014 % total=> 8.44212 %

83: 429 141224 <=> 146412 5.16867 per gap=> 8.26988 % total=> 8.64562 %

84: 457 146412 <=> 151725 5.44048 per gap=> 8.60154 % total=> 8.27378 %

85: 447 151725 <=> 157165 5.25882 per gap=> 8.21691 % total=> 8.59707 %

86: 461 157165 <=> 162734 5.36047 per gap=> 8.27871 % total=> 8.21762 %

87: 458 162734 <=> 168432 5.26437 per gap=> 8.0372 % total=> 8.27597 %

88: 489 168432 <=> 174262 5.55682 per gap=> 8.38765 % total=> 8.04114 %

89: 501 174262 <=> 180225 5.62921 per gap=> 8.40181 % total=> 8.38781 %

90: 511 180225 <=> 186322 5.67778 per gap=> 8.38048 % total=> 8.40158 %

91: 505 186322 <=> 192556 5.54945 per gap=> 8.10139 % total=> 8.37745 %

92: 524 192556 <=> 198927 5.69565 per gap=> 8.22477 % total=> 8.10271 %

93: 522 198927 <=> 205437 5.6129 per gap=> 8.01843 % total=> 8.22257 %

94: 562 205437 <=> 212088 5.97872 per gap=> 8.45049 % total=> 8.02298 %

95: 536 212088 <=> 218880 5.64211 per gap=> 7.89106 % total=> 8.44466 %

96: 572 218880 <=> 225816 5.95833 per gap=> 8.24683 % total=> 7.89472 %

97: 579 225816 <=> 232897 5.96907 per gap=> 8.17681 % total=> 8.24611 %

98: 566 232897 <=> 240124 5.77551 per gap=> 7.8312 % total=> 8.17332 %

99: 597 240124 <=> 247500 6.0303 per gap=> 8.09437 % total=> 7.83383 %

100: 610 247500 <=> 255025 6.1 per gap=> 8.10631 % total=> 8.09448 %

101: 605 255025 <=> 262701 5.9901 per gap=> 7.88171 % total=> 8.10411 %

102: 640 262701 <=> 270530 6.27451 per gap=> 8.17526 % total=> 7.88456 %

103: 632 270530 <=> 278512 6.13592 per gap=> 7.91732 % total=> 8.17278 %

104: 649 278512 <=> 286650 6.24038 per gap=> 7.97493 % total=> 7.91787 %

105: 642 286650 <=> 294945 6.11429 per gap=> 7.7396 % total=> 7.97271 %

106: 663 294945 <=> 303398 6.25472 per gap=> 7.84291 % total=> 7.74057 %

107: 677 303398 <=> 312012 6.3271 per gap=> 7.85976 % total=> 7.84306 %

108: 723 312012 <=> 320787 6.69444 per gap=> 8.23932 % total=> 7.86324 %

109: 712 320787 <=> 329725 6.53211 per gap=> 7.96599 % total=> 8.23683 %

110: 720 329725 <=> 338828 6.54545 per gap=> 7.90991 % total=> 7.96548 %

111: 722 338828 <=> 348096 6.5045 per gap=> 7.78983 % total=> 7.90884 %

112: 734 348096 <=> 357532 6.55357 per gap=> 7.77872 % total=> 7.78973 %

113: 755 357532 <=> 367137 6.68142 per gap=> 7.86049 % total=> 7.77944 %

114: 747 367137 <=> 376912 6.55263 per gap=> 7.64155 % total=> 7.85859 %

115: 768 376912 <=> 386860 6.67826 per gap=> 7.72053 % total=> 7.64223 %

116: 790 386860 <=> 396981 6.81034 per gap=> 7.80555 % total=> 7.72126 %

117: 772 396981 <=> 407277 6.59829 per gap=> 7.49806 % total=> 7.80295 %

118: 818 407277 <=> 417750 6.9322 per gap=> 7.81093 % total=> 7.50069 %

119: 821 417750 <=> 428400 6.89916 per gap=> 7.70856 % total=> 7.81008 %

120: 848 428400 <=> 439230 7.06667 per gap=> 7.8301 % total=> 7.70956 %

121: 849 439230 <=> 450241 7.01653 per gap=> 7.71047 % total=> 7.82912 %

122: 840 450241 <=> 461434 6.88525 per gap=> 7.50436 % total=> 7.7088 %

123: 880 461434 <=> 472812 7.15447 per gap=> 7.73456 % total=> 7.50621 %

124: 898 472812 <=> 484375 7.24194 per gap=> 7.76615 % total=> 7.73482 %

125: 898 484375 <=> 496125 7.184 per gap=> 7.64255 % total=> 7.76517 %

126: 901 496125 <=> 508064 7.15079 per gap=> 7.54701 % total=> 7.6418 %

127: 928 508064 <=> 520192 7.30709 per gap=> 7.6514 % total=> 7.54783 %

128: 940 520192 <=> 532512 7.34375 per gap=> 7.62987 % total=> 7.65123 %

129: 937 532512 <=> 545025 7.26357 per gap=> 7.48821 % total=> 7.62878 %

130: 952 545025 <=> 557732 7.32308 per gap=> 7.49164 % total=> 7.48824 %

The increasing number of primenumbers between those gaps. That’s adding.

I have also 400 results.

With friendly regards,

Dirk-Anton Broersen

Ps. According to my last email, this maybe not the wright approach. I came in this group it seems and how I received your mail, that’s the question. But I like to be in a math-group.

Verzonden vanuit Mail voor Windows 10

Van: Dirk-Anton Broersen
Verzonden: dinsdag 24 maart 2020 13:08
Aan: meta...@googlegroups.com; Dirk-Anton Broersen
Onderwerp: Re: [Metamath] Formalizing IMO B2.1972

I'm also a beginner. And I received this email. I posted lately an email about a finding. I don 't know of it's unique or known or if it has resemblance.

It's also about triangelar numbers in a formula.

E

x = x + 1

(triangelar number) power 2 / x

triangelar number = triangelar number + triangelar number + 1

First results are and I also wrote a programm in c++ wich you can copy paste to cpp.sh to see the results.

1 1 (1/1) 1 = 1 ^2

2 4.5 (9/2) 9 = 3 ^2

3 12 (36/3) 36 = 6 ^2

4 25 (100/4) 100 = 10 ^2

1 <==> 4.5 <==> 12 <==> 25 <==> ..

within these gaps there is an amount of primenumbers that inscrease. Percentual it's also intersting.

I'll send next the first number of results of the programm. then it's also clear what number of primes are increasing.

Including the programm.

I don 't wanna frustrate others work. This might be seen as trolling. I just received this email, but I tought this might be something. I'm an undergraduated mathematician. And it has also to do with triangelar numbers.

With friendly regards,

Dirk-Anton Broersen

Outlook for Android downloaden

Thierry Arnoux

unread,

Mar 24, 2020, 10:21:05 AM3/24/20

to meta...@googlegroups.com, Dirk-Anton Broersen

Hi Dirk-Anton,

This list is more for formalization of mathematics in Metamath; other mailing lists are probably more adequate, like alt.math.undergrad (http://mathforum.org/library/view/6791.html ).

Anyway, if you are interested in how prime numbers are distributed, you should check the prime number theorem (https://en.wikipedia.org/wiki/Prime_number_theorem?wprov=sfti1).

Furthermore, here is what I would suggest:

You may be able to write your sequence in a closed form. You define it as A_n=(T_n)^2/n, where Tn is the nth triangular number. There is a closed form for the triangular numbers: Tn = n(n+1)/2, and if you inject it in A_n, you get A_n = n(n+1)^2/4.

Then, using the prime number theorem, you may be able to estimate how many primes are lower than or equal to A_n; how many are less than A_(n+1), and by difference, how many primes are between A_n and A_(n+1), and finally, you could check if this agrees with the limit you get experimentally by counting.

BR,

_

Thierry

Envoyé de mon iPhone

Van: Dirk-Anton Broersen
Verzonden: dinsdag 24 maart 2020 13:08
Aan: meta...@googlegroups.com; Dirk-Anton Broersen
Onderwerp: Re: [Metamath] Formalizing IMO B2.1972

I'm also a beginner. And I received this email. I posted lately an email about a finding. I don 't know of it's unique or known or if it has resemblance.

It's also about triangelar numbers in a formula.

E

x = x + 1

(triangelar number) power 2 / x

triangelar number = triangelar number + triangelar number + 1

First results are and I also wrote a programm in c++ wich you can copy paste to cpp.sh to see the results.

1 1 (1/1) 1 = 1 ^2

2 4.5 (9/2) 9 = 3 ^2

3 12 (36/3) 36 = 6 ^2

4 25 (100/4) 100 = 10 ^2

1 <==> 4.5 <==> 12 <==> 25 <==> ..

within these gaps there is an amount of primenumbers that inscrease. Percentual it's also intersting.

I'll send next the first number of results of the programm. then it's also clear what number of primes are increasing.

Including the programm.

I don 't wanna frustrate others work. This might be seen as trolling. I just received this email, but I tought this might be something. I'm an undergraduated mathematician. And it has also to do with triangelar numbers.

With friendly regards,

Dirk-Anton Broersen

Outlook for Android downloaden

<77609AC6AB764EF7881D5C907B5BE9D9.png>

From: 'Stanislas Polu' via Metamath <meta...@googlegroups.com>
Sent: Monday, March 23, 2020 9:05:17 PM
To: meta...@googlegroups.com <meta...@googlegroups.com>
Subject: Re: [Metamath] Formalizing IMO B2.1972

Hi Marnix!

Thanks for sharing. The proof I formalized[0] is very closed but I agree is also a bit more complicated.

Out of curiosity, where did you find that proof which has a very "formal" presentation?

Best,

-stan

[0] http://us.metamath.org/mpeuni/imo72b2.html

On Mon, Mar 23, 2020 at 6:38 PM Marnix Klooster <marnix....@gmail.com> wrote:

Hi Stan,

If I were to formalize this in Metamath, I'd use the first proof, but in a more calculational format.

I've attached it, unfortunately as a picture.

Yes, this is a longer proof, but it seems somehow easier to me.

Hope this helps someone... :-)

<image.png>

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/VI1P18901MB073396470DC49544F854329583F10%40VI1P18901MB0733.EURP189.PROD.OUTLOOK.COM.

Dirk-Anton Broersen

unread,

Mar 24, 2020, 12:14:11 PM3/24/20

to meta...@googlegroups.com

Dear Thierry,

I’ll have a look on the prime number theorem, because I think it also implies on primegaps and how they are distributed,

And those findings on my result were somehow diffirent. For example 10^1 or 10^x.

Mine are distributed somehow diffirent and here’s that results.

In the second line you see how the primenumbers in between are growing. The gaps are also growing with the formula. What I think is sort of exponential.

Maybe I can’t read it to well to see some resemblance. Those prime ”pakkeges” are growing nicely,

And I’ll try to create a formula in a mathematical way,

And to find out if there’s some resemblance and so if there maybe is a diffirence..

They seem to ditribute and grow evenly.

This is made in C++ by me

Results.

131: 971 557732 <=> 570636 7.41221 per gap=> 7.52509 % total=> 7.49189 %

132: 999 570636 <=> 583737 7.56818 per gap=> 7.62537 % total=> 7.52584 %

133: 1009 583737 <=> 597037 7.58647 per gap=> 7.58647 % total=> 7.62508 %

With friendly regards,

Dirk-Anton Broersen

Verzonden vanuit Mail voor Windows 10

Marnix Klooster

unread,

Apr 30, 2020, 4:28:52 AM4/30/20

to Metamath

Hi all,

For the record, there are two (related) mistakes in my write-up (the picture in my March 23 email):

The properties (0) and (1) of sup are of course only correct for upper-bounded V.
Therefore in the steps where we use these properties, we need to know that |f| and |f*g| are upper bounded, so we do use the |f|≤1 assumption.

And the good news is that I discovered these when studying Stan's http://us.metamath.org/mpeuni/imo72b2.html. :-)

Groetjes,

<><

Marnix

Op ma 23 mrt. 2020 om 18:38 schreef Marnix Klooster <marnix....@gmail.com>:

--

Marnix Klooster
marnix....@gmail.com

Stanislas Polu

unread,

Apr 30, 2020, 4:59:15 AM4/30/20

to meta...@googlegroups.com

Formal systems for the win \o/

-stan

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAF7V2P9BKgAORpE2j6COqZmqD%2B7R5yHfZPnUg3Qpk4DQ3D0ZXQ%40mail.gmail.com.

Reply all

Reply to author

Forward