Computer-assisted proofs were a mistake

>nature.com/news/two-hundred-terabyte-maths-proof-is-largest-ever-1.19990
>The puzzle that required the 200-terabyte proof, called the Boolean Pythagorean triples problem, has eluded mathematicians for decades. In the 1980s, Graham offered a prize of US$100 for anyone who could solve it. (He duly presented the check to one of the three computer scientists, Marijn Heule of the University of Texas at Austin, earlier this month.) The problem asks whether it is possible to color each positive integer either red or blue, so that no trio of integers a, b and c that satisfy Pythagoras’ famous equation [math] a^2 + b^2 = c^2 [/math] are all the same color. For example, for the Pythagorean triple 3, 4 and 5, if 3 and 5 were colored blue, 4 would have to be red.
>The numbers 1 to 7,824 can be colored either red or blue so that no trio a, b, and c that satisfy [math] a^2 + b^2 = c^2 [/math] are all the same color. The grid of 7,824 squares here shows one such solution, with numbers colored red or blue (a white square can be either). But for the numbers 1 to 7,825, there is no solution.
>There are more than [math] 10^2300 [/math] ways to color the integers up to 7,825, but the researchers took advantage of symmetries and several techniques from number theory to reduce the total number of possibilities that the computer had to check to just under 1 trillion. It took the team about 2 days running 800 processors in parallel
>arxiv.org/abs/1605.00723

And it only cost them $504,000 in electricity to win that $100.
>CS professors in charged of mathematics

Other urls found in this thread:

nation.co.ke/news/Groups-want-trade-barriers-removed-to-spur-Africa-growth/-/1056/2996774/-/dke3v0z/-/index.html
youtu.be/a1zDuOPkMSw?t=13m34s
eia.gov/electricity/monthly/epm_table_grapher.cfm?t=epmt_5_6_a
en.wikipedia.org/wiki/Experimental_mathematics
tacc.utexas.edu/stampede/
twitter.com/NSFWRedditGif

>CS professors in charged of mathematics

can we agree that brute forcing problems isn't that cool

I think it's pretty cool to be able to force a problem, it shows how much power we got.

But with that $500K you could have feed 140k starving African children for a whole month.

>CS professors in charged of mathematics
>you could have feed 140k

>autists in charge of speech

what country in africa?
it doesn't matter, if you want to help some starving person, stop taking shit from them instead of stroking your ego by throwing a tiny fraction of what you take from them.

it's not about the money, it's about asserting dominance :^)

>feed
>not invest

Give a man a fish blah blah blah...

That problem sounds so specific. Does it have any uses? I feel like you could come up with an infinite amount of specific hard to solve problems.

>get 7 kids on average
>starve
feeding them only makes the problem worse

It is very easy to come up with hard problems but much more difficult to come up with hard problems that have answers. That makes the ones that have answers far more cool.

Is that what mathematicians do? Spend years trying to solve some obscure problem?

I would rather buy them crop seeds, herds or investments for businessess

nation.co.ke/news/Groups-want-trade-barriers-removed-to-spur-Africa-growth/-/1056/2996774/-/dke3v0z/-/index.html

cut subsidies for western farmers (they basically only cost money to your societies anyway).
Subsidies allow them to sell for less than african farmers with no subsidies, starving them because they can't sell their production.
You can buy them all the seeds you want, they can't benefit. Charity is just a coping mechanism to feel better.

I warned you about computer assisted proofs, bro. I told you it would end like this. I told you dawg.

2000 years of mathematics and we are slacking. Humanity needs to get their shit together again.

It's what people in literally every field do. If you go to something that sounds super useful like "curing cancer" but then look at what individual scientists are doing you'll find it's often something pretty useless sounding. But the point of research is you don't really know what is useful or hard until you try it.

>But with that $500K you could have feed 140k starving African children for a whole month.

My best guess is that those 500k came in some kind of grant.

Call me a lunatic, but I do not think that african children can apply for research grants so that money would literally never feed starving children, you retard.

Who pays them to do the useless sounding research though?

You do. Deal with it.

...

No, mathematicians learn how to investigate interesting problems.

>cut subsidies for western farmers (they basically only cost money to your societies anyway).

but it's good to be somewhat self sufficient.

>says the gook
kek

Yeah, let's only study things we already understand. That sounds like a great way to keep up the breakneck pace of scientific progress we've enjoyed in the last few decades.

>The numbers 1 to 7,824

So it's not even a real, general proof or does 7824 have any significance?

I am genuinly curious because I myself would like to research some useless things but I thought you can't do that since someone will only pay you if it's profitable.

that's not how research works.

research does not need to have immediate applications. its goal is to broaden our understanding, to test theories, to gather data, to test new potential technologies etc

R&D on the other hand has profitability in mind. A lot of stuff from R&D today comes from the public research of yesterday.

And that's why research is paid by public funding in normal countries, while R&D is financed by companies.

The NSF or similar organizations, which usually come from taxpayer money.

You gotta at least be able to convince people in your own field that your problem is interesting though

I assume they had some general proof that showed that if you have a coloring that works for those then you can extend it to a coloring of all integers

youtu.be/a1zDuOPkMSw?t=13m34s

They showed there isn't any coloring past 7824

Can you elaborate on how exactly it works? I assume you present what you want to research, the expected costs and then you get a grant for a certain period of time after which you need to present results and convince to pay you to continue the research?

Computer assisted proofs are not legitimate, imo. You need to be able to prove it analytically. Forex, the four color theorem hasn't been proved.

do you forget that we are biological creations of random accidents?

A hundred years ago Marie Curie was playing with uranium with her bare hands, are we expected to solve every math problem with only our brains.

This is only surprising to plebs who aren't familiar with Ramsey theory

>And it only cost them $504,000 in electricity to win that $100.
who pays for this exactly?

you do, dear undergrad. thanx for the the tuition monies, now try to make something of this engrish-as-a-second-language lecturer.

Aren't you really complaining about proving by counter example?

The fact that this proof happened to use a computer to find a number for which the statement was not true is irrelevent.

Why am I supposed to care about Africans again? What is so important about Africa's contribution to society that I need to help their poor? Why can't I help poor Asians, Americans, or Europeans?

wait, wait, wait...

Hold on.

They actually ran the program? They actually spent money on the electricity?

If they're computer scientists, why would they need to run the program and actually spend money on the electricity if they can just know what the output of the program will be analytically? What the fuck is the point of computer science if they can't tell us what the output of the program will be before running it? Why would they waste half a million dollars on something they should only need chalk and some ingenuity?

Isn't the whole point of computer science ... the whole point being so you DON'T have to run the programs and waste money on electricity to see if the results are correct?

Am I missing something here? What the fuck?

You are definitely missing something here. E.g. analytically we can tell that a sorting algorithm will always output a sorted list, but to get an explicit output for a given input, generally you need to use the algorithm itself.

They didn't have a way to analytically check every single possible combination, are there were far too may possibilities to check it manually.

>Retardation: The Post

CS/SE undergrad dropout detected

> A fundamental question is whether Theorem 1 has a “mathematical” (human-readable) proof, or whether the gigantic (sophisticated) case-distinction, which is at the heart of our proof, is the best there is? It is conceivable that Conjecture 1 is true, but for each k has only proofs like our proof, where the size of these proofs is growing so quickly, that Conjecture 1 is actually not provable in current systems of foundations of Mathematics (like ZFC).

>implying I graduated high school

rofl

> analytically we can tell that a sorting algorithm will always output a sorted list,

that doesn't tell me anything useful about the function we're working with. I need to know what sequences of triplets don't work. what compositions are outside the domain. a list gives me a list? groundbreaking. really narrows it down.

>analytically check every single possible combination
>analytically check all solutions
>analytically check all
>analytically
>all

yeah have fun "analytically checking all the solutions". tell me when you've finished that rainman

>has to spend 500k to figure out an upper bound

It's almost like we don't know anything about numbers and don't know how to eliminate certain types of solutions based on the properties of those numbers and the properties required by the rule of the function. I mean, we don't really know nuffin right? computers are the only things that know anything right? would it really be that hard to ... i dunno, prove whether we can even get any solutions on say, odd triplets, even triplets, (odd,even,odd) triplets, (o,o,e) triplets, etc.

you know, getting rid of all the wrong answers ... first... might ... you know... give us a smaller domain to work with so we're not counting every single fucking number.

>using ZFC

jesus

>get 7 kids on average
>have multinational corporations steal 100% of the countrys natural resources while only paying a token fee to a completely corrupted government.
>starve

Altruism is the downfall of modern western society.

The best part about any conversation about whether or not we should help Africans is that both sides are implying they need help, yet neither realizes it!

>have fun checking all the solutions
>there are too many solutions
The dangers of being a faggot

>caring about people and things that will never affect your life if you don't want it to

>48 hours
>800 processors
>lets say 200 watts per processor (that's a high power processor)
>200 * 800 * 48 / 1000 = 7,680 kilowatt hours
>$504,000 / 7,680 = 65.625 $ per KWH
>US average cost per KWH is $0.1234 residential and $0.1027 all sectors
eia.gov/electricity/monthly/epm_table_grapher.cfm?t=epmt_5_6_a

>you're saying they payed 531.81 times the average residential electric price

though to be fair the 200 TB of hard drives must have cost a lot
i found some 2 TB ones on ebay for $35 and at that price it would cost $3,500
that plus the ~ $1,000 in electrics puts us at ~$4,500

>that's a total cost of 112 times less than what you said

>he thinks cost is only raw materials

protip: in science like that, most of the cost is work time.

kill yourself brainlet

>most of the cost is work time
>brute force
r u srs m8
besides the point was that it cost no where near $504,000

>kill yourself brainlet
make me.
If you can get your fat ass out of your chair to get your teeth knocked out.

What the hell am I personally taking from some unknown person in Africa?

>brainlets resort to physical violence when threatened intellectually
heh

>manletobrainlets resort to "kys" when they don't understand anything

I can feel your assblast though.
go where you belong.

>if others do it on my behalf, I am not accountable

>found the nigger
But really, whats wrong with china? they've come a long way despite being their history of being screwed by the west, and the far east
Also a gook is a Korean, Chinese are chinks.

despite their history*
oy vey

I do not know what video this scene is from but the asian guy seems to either be ignorant of the concept concerning the diffusion of innovations or wants to capitalize on the black guy's lack of knowledge of said concept in that conversation.

Just because a country or population becomes occupied by a foreign power does not mean said foreign power's ideals and technology will successfully take root into the populous.

They learn from the best.

> despite their history
Their history of being the baddest on the block East of the Eurasian Steppe?

>Also a gook is a Korean, Chinese are chinks.
they look the same
they live like trash and try to tell niggers they also live like trash.

>Their history of being the baddest on the block East of the Eurasian Steppe?
I was thinking more of western spheres of influence, Opium, Jap invasion, perpetual civil war and revolutions, but yeah..
Baddest.
Stay mad nigger, the chinks will rule over you for centuries to come. Chinese people dont live like trash. Koreans are dirty, loud and rude

>Stay mad nigger, the chinks will rule over you for centuries to come. Chinese people dont live like trash. Koreans are dirty, loud and rude
kek
I'm not even african nor am I black
but hey, at least you tried with your poor ad homniem

Chinese people can't even breathe their air, and can't drink their water and die working like slaves for us.

>uses ad hominem
>gets ad homimemed
>haha nice ad hominem fag XDDDD
Ayyyyyyyy

Exactly

>I was thinking more of western spheres of influence, Opium, Jap invasion, perpetual civil war and revolutions, but yeah..
So just the last 200 years....gotcha

>mad

REEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEE

>whats wrong with china? they've come a long way despite being their history of being screwed by the west

You do know China was the most advanced culture on Earth for most of civilised history, right?

>yfw you realize experimental mathematics is actually a thing

en.wikipedia.org/wiki/Experimental_mathematics

What do you mean, analytically ?

The four color theorem's proof could be done by a human on paper. It would just be extremely boring, and very likely that he would forget some cases and stuff. But computer-assisted proofs is the same notion of "proof" than what mathematicians publish.

zfc has case disjunction

wtf

>proof by counterexample isn't legitimate

it means the complete, all-cases proof is infinitely long. an infinitely long proof isn't a valid proof.

>colonialism should be fragile, nice and smooth

call me when a computer solves the syracuse problem or the traveling salesman problem

what

you're saying those that got conquered have the right to reparations, right?
why is that
they got conquered, they should have no say

processors
>>lets say 200 watts per processor (that's a high power processor)
>160kW

>tacc.utexas.edu/stampede/
>Max Power Usage: 4.5 Megawatts
>Average Power: 3 MW

So it's 4.5*48*1000 = 216,000 kWh at a total cost of $26.7K

no, I'm saying if you want to help someone, you should pay them a fair price for what they give you right now.

>give us right now
nothing?
some help I can think of is letting the starve (so no dependent population on aid) and also taking their land so we can put it to good use, so that it maybe helps them

>implying I graduated high school

rofl

> analytically we can tell that a sorting algorithm will always output a sorted list,

that doesn't tell me anything useful about the function we're working with. I need to know what sequences of triplets don't work. what compositions are outside the domain. a list gives me a list? groundbreaking. really narrows it down.

>analytically check every single possible combination
>analytically check all solutions
>analytically check all
>analytically
>all

yeah have fun "analytically checking all the solutions". tell me when you've finished that rainman

>has to spend 500k to figure out an upper bound

It's almost like we don't know anything about numbers and don't know how to eliminate certain types of solutions based on the properties of those numbers and the properties required by the rule of the function. I mean, we don't really know nuffin right? computers are the only things that know anything right? would it really be that hard to ... i dunno, prove whether we can even get any solutions on say, odd triplets, even triplets, (odd,even,odd) triplets, (o,o,e) triplets, etc.

you know, getting rid of all the wrong answers ... first... might ... you know... give us a smaller domain to work with so we're not counting every single fucking number.

>confining yourself a single framework
>wonders why there are limitations

Gee...

Post got deleted? What? My /pol/ bait doesn't get deleted but my sincere questions about cs do? rofl.

Oops. Realized the "implying i graduated hs" was misinterpreted as "I am not older than 18". Sorry janitor, I meant to say, "I am an adult that didn't graduate high school". I see why that was unclear.

Didn't you already post this?

A proof is a proof and sometimes you need case distinctions

oh you so cool user, I want to hang out with you. What a strong and intelligent man you must be.

>n-edgy-(n+2)-me

Africa is the richest continent on earth (in term of ressources) any civilization would thrive in this conditions, the only problem with africa is the africans. We even gave them a fully developped infrastructure for free and they still manage to starve for fuck sake. Every $ spend on charity for africa is a $ wasted.

whatever, go back to reading about how Africans are developed and have the same mental capacities as whites in the west
go ahead, they just need more money they're in a rough spot, after all, the white man kept them down, colonialism stole their potential, Danm those whities
they were Egyptians, they were kings

oh you so cool user, I want to hang out with you. What a strong and intelligent man you must be.

>n-edgy-(n+2)-me

...

>if you can't refute it, just say "", you'll win then

>there is nothing to refute
>but at least you can't refute it

I imagine you like the average fatass at home thinking it's bad to offend people
go kill yourself, cuckold

>projecting this hard
top
kek

>$504,000 in electricity
I wonder how much that would've cost in wadges if you had a bunch of people trying to solve it.

> im a dumb sjwtard shitter please rape my face