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: [email protected]; 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 <[email protected]> > Sent: Monday, March 23, 2020 9:05:17 PM > To: [email protected] <[email protected]> > 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 <[email protected]> > 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> > > > Groetjes, > <>< > Marnix > > Op do 27 feb. 2020 om 18:08 schreef 'Stanislas Polu' via Metamath > <[email protected]>: > 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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/78223c8d-eddf-4f84-970d-6b0cbb20dab9%40googlegroups.com. > > > -- > Marnix Klooster > [email protected] > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/CAF7V2P-2gAJsLSmnz-AtneyXNOGmG5w%3Dcn2gYVXk94FUQ5XdPg%40mail.gmail.com. > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/CACZd_0x56Ck-geksHLs0pRZwCLb_oaisqxyFpH4Ds5haXkrU9Q%40mail.gmail.com. > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/VI1P18901MB073396470DC49544F854329583F10%40VI1P18901MB0733.EURP189.PROD.OUTLOOK.COM. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/BCBD5139-3160-47E9-9B92-B8743C61AF19%40gmx.net.
