I am not sure about my claim. I thought I recalled that being done, but I may be mistaken.
Here is some earlier work that addresses books I to IV:
https://www.andrew.cmu.edu/user/avigad/Papers/formal_system_for_euclids_elements.pdf
I am not sure about my claim. I thought I recalled that being done, but I may be mistaken.
Here is some earlier work that addresses books I to IV:
https://www.andrew.cmu.edu/user/avigad/Papers/formal_system_for_euclids_elements.pdf
Has chess been solved? No
Can chess be solved? Yes, it takes 5 years on cloud engines.
Will chess be solved? Maybe, it depends on somebody paying 5 million $ for the cloud engines and the human assistants during 5 years.
Have humans walked on Mars? No
Can humans walk on Mars? Yes
Will humans walk on Mars? Maybe, it depends on somebody paying billions of $ to build and launch a spacecraft.
That is post 2 of this forum - three months ago and over 3000 posts ago.
There's an attempt at an analogy between solving chess and a manned mission to Mars.
That doesn't prove anything of course.
And in that post @tygxc doesn't qualify with 'weakly' solving.
Its a kind of 'provocative dogbone'.
Has @tygxc conceded anything at all yet?
Has he conceded that 'strong' solving isn't feasible?
Not exactly. In his post 2 he didn't specify 'strong'.
So no. Nothing conceded. Not one point.
Regarding 10 to the 9th power computer - implying a billion positions solved per second - that doesn't hold up at all.
I didn't say he said that though.
A node isn't a 'position solved'.
If the computer could do a billion 'somethings' per second ...
and you put that up against 10 to the 44th positions.
Even if - the 'something' was solving a position -
it would still take 10 to the 35th seconds.
Which is more than 3000 trillion trillion years.
If it was 10 to the 37th positions ... then it would still take over
30 million trillion years.
But a node is not 'solving a position' ...
so it would take a lot longer than 30 million trillion years.
@tygxc is essentially still maintaining that 'it'
"takes 5 years on cloud engines.".
He has the same position 3 months later.
But what is 'it' ?
'It' may be nothing.
If solution is to be 'weak' that could mean chess already is solved as in
"chess is a draw unless somebody makes a mistake that can be exploited enough to force a win - except when that's not the case and its a win anyway"
In which case 5 years and cloud computers are both irrelevant.
So with a range of 'weak' possibilities that extends from 'already solved' all the way up to much more than 30 million trillion years -
then 5 years and cloud computers is random and arbitrary.
Another way to say this:
Could all of @tygxc's posts be 'skipped' except for his first posting here five years ago ? Because they're all essentially repetitions.
And post 2 at best is saying that chess can be solved but it could take over 30 million trillion years to do so.
And since the number of possible positions is finite -
then indeed it could be. And can be.
No bogus time needs to be added to support a possibility of 'solved'.
Its a finite number of positions - so it can be solved.
But that doesn't mean it will be.
Point: @tygxc 's post can be divided into two sections.
Concerning a possibility of solving - but that's already known because the number of positions is finite.
What's he's trying to do is argue that it can be solved by assigning a bogus time to it. Its like he's venturing a proof by assigning an unfounded time period.
Can the Andromeda galaxy be reached?
Yes. 'It takes two months using faster than light travel.'
If that had been his initial post in a forum about reaching Andromeda - how much response would that have deserved and gotten?
None. So what's actually different about his post 2?
Cloud computers exist whereas faster than light travel doesn't?
Doesn't hold up.
Space travel exists - but no computers exist that can solve a billion positions per second.
So it looks like his post 2 fails. It makes an assertion with no basis.
Still - it gets a lot of attention anyway
Maybe that will continue.
I am sure the phrase was 'provability is a higher degree of truth'. It figured in a feature article in Scientific American about unsolved mathematical problems including at that time Fermat's Last Theorem. It also discussed ramifications of Gödel's incompleteness theorems.
I cannot unfortunately provide volume, no., or page: I have no eidetic memory allowing total recall.
Then concede to take that statement as unreferenced. Anyway, if the statement was true, a proof could not be true at a higher degree than a knowledge already 100% true, and an axiom cannot be used to prove the axiom itself, like you do.
"and an axiom cannot be used to prove the axiom itself, like you do."
'trying' to do. For three months.
Failing - but controlling the forum anyway.
and he's got Nerve - pushing same.
Is another 1000 posts of that coming up ?
Not only "could", pretty sure that has been done. I think all of Euclid has been mechanised. Here is a paper about mechanical verification of book I.
I put the link in my home page notes. So I could get around to reviewing that site sometime.
Regarding putting mathematical history on a timeline - creating a timeline in other words - its much easier to do that nowadays than in pre-internet times.
Regarding math and proofs being 'mechanized' it might be useful to know what isn't mechanized - or not yet. Or what can't be.
In a way - the discussion of solving chess is a bit like discussion of the future history of mathematics.
Chess apparently wasn't designed to have a relation to math though.
It was a game of royalties and generals and merchants and nobles is what I've read. And scribes and clergy.
Don’t rely on links for everything. It’s best to keep up the mathematics and not use links as examples.
🙁
“Playerafar wrote:
Chess apparently wasn’t designed to have a relation to math though
I think there’s more to it than that
Elroch wrote: Not only "could", pretty sure that has been done. I think all of Euclid has been mechanised. Here is a paper about mechanical verification of book I.
Oh, please
“Playerafar wrote:
Chess apparently wasn’t designed to have a relation to math though
I think there’s more to it than that
Which is what my post suggests. Something else.
And 'wasn't' is past tense.
Don’t rely on links for everything. It’s best to keep up the mathematics and not use links as examples.
🙁
Hi !
Who said 'rely' ?
By the way - welcome to chess.com.
You having joined the site yesterday.
Regarding the 50 move rule - it can be considered an adjunct to chess -
like the issue of what is 'mating material' when somebody's flag falls in a sudden death game.
If the side whose flag didn't fall has an apawn or hpawn in a dead drawn position - then that side wins. For example.
In a situation where the 50 moves is counting - the exact number of moves left dictates strategy.
Especially for the defending side.
The rule could determine whether the position is a win or a draw anyway though. With or without strategy.
But that should be Skipped by the initial computer bank and Skipped as initial goal.
It should be skipped as Secondary goal too.
Should be low on the priority list. Lowest? Not necessarily.
///////////////////////////////
In a correct way to go at the hypothetical project -
I say - mating material and 50 move rule and repetitions of position are skipped. (a possibility of a repetition of position - if there's already been a 2-fold repeat - could again determine strategy. But could also determine whether its a draw or win because a defending side could perhaps force a final repetition)
But that should also be skipped in the initial stages too.
(nobody else in these forums has confirmed yet that he/she understands why.)
In other words - such a project would be done in Stages.
Multiple computers or banks of computers assigned.
So the first computer bank's job is to generate positions - not games.
Arrangements of pieces which do provide for either side to move.
(Otherwise they'd be the so-called 'diagrams'. Not good enough.)
Does that mean there's already a legality issue?
In some positions - it would be impossible for either side to move.
For example white's g-knight at f3. Every other piece at its home square.
Would it be possible for it to be white's move? I don't know.
Is there a sequence of moves that would bring that about ?
Should these issues of 'could it have got there legally?' be left out in the initial stages of the project ?
That's harder.
It depends on how positions to be solved are to be generated.
Somehow - simplicity has to be maintained - but without the ridiculous premises being pushed over and over again by @tygxc .
That's not personal. Simply addresses his posts.
Approach - define the initial goal for the initial computer bank.
Assign other relevant tasks to backup computer banks.
Suggestion for that initial goal:
A computer bank proceeds with position generation.
It then classifies every position it generates into categories and then refers each category to the appropriate secondary computer bank.
Of which there might be several.
And like the issue of whose move it is - castling and en passant should be provided for but not in a way that confounds and cripples the initial goals.
Other computer banks get those positions -
further down the Goals priority list.
Many ways to set up those Categories.
Part of solving - classifications of positions.
Links up Hugely with actual chessplaying.
But both the position generation and the classifications would be designed to fit with and greatly enhance the efficiency and effectiveness of the different computer algorithms assigned to each category.
That would be Top Priority.
Without such stages - the whole project degenerates.
#3026
"If you say "there is no doubt", then it's 100% sure and thus proven."
++ When something is known, then there is no doubt, it is 100% sure, but the proof may not be available.
We know 1 e4 e5 2 Ba6? loses for white, there is no doubt, but there is no proof that works out all possible variations to checkmate. Proving it poses no problem, but it is not worthwhile to burn computer time on it, precisely because the outcome is not in any doubt.
Likewise we know 1 a4 is not superior to 1 d4 or 1 e4. Capablanca said so: 1 e4 and 1 d4 accomplish more than 1 a4. AlphaZero concurs.
No. AlphaZero outputs probabilities. It is uncertain about the outcome of every move (except where complete analysis to a result is possible). The move that it assesses to have a higher probability of a good result, it views as better. It is sometimes wrong (to the extent that its decisions lose).
And Capablanca is less reliable than AlphaZero.
But @tygxc is probably not. He has only to state something to consider it proven.
I don't know about AZ, but I just downloaded SF15 and it seems that you can't even know when it is certain.
I wanted to see at what level it became out of it's depth in KNNKP so I let it play a mate in 36 position and it drew by repetition after 14 moves. The following image shows SF15 announcing mate in 38 (full) moves from the initial position while simultaneously showing a search depth on the same line of only 33 half moves! It lasted for a few seconds then it changed its mind to 0.80 and after another second or so to 0.00.
Incidentally we seem to again show minimax pathology at work.
I first ran the kibbitzer until the top line showed depth 48 and captured the top line, which is inserted into the game log. Notice this follows the game until Black's move 3 when it contains 3...Kg6 instead of 3...Kh5 which I played. The kibbitzed move would slip 3 moves on the move I played which is accurate. However in the later version (bottom) which has reached only depth 33 it is showing 3...Kh5.
"But @tygxc is probably not. He has only to state something to consider it proven."
That's correct. And then he repeats it over and over. As if repetition is proof.
And again - without being personal - its similiar to the positions of flat-earthers.
They simply make assertions. And therefore/thereby consider them correct.
In tygxc's case he'll mention Sveshnikov or den Herik and also then take a position that mentioning their names is additional 'proof'.
The flat-earthers are on the rise in numbers.
Especially among millenials.
There may be a corresponding and growing cult that believes that anything can be done with computers.
#3071
"He has only to state something to consider it proven."
++ I am the only one who provides proofs and references.
Some people do not understand the proofs and then deny it being a proof.
All other people state something without any proof at all.
Chess is already strongly solved for 7 men or less.
There is no point in rehashing 5 men positions.
"AlphaZero outputs probabilities." ++ AlphaZero autoplay yields results.
"Capablanca is less reliable than AlphaZero."
++ Capablanca was human and provided human insight
I am the only one who provides proofs and references.
You repeated this many times, but it's plainly false. Several posters have proven or disproven concepts and provided references. You did not prove your ideas because the "proofs" are flawed.
To start, you use a supposedly known but not proven game-theoretic value of the game (a draw), to "deduce" (after other fallacies and mistakes) an error rate per move. I asked you to give a reference of a scientific work where the authors claim they know something which is not either proven, or at least never disproven by a history of experiments. You provided only a statement: "provability is a higher degree of truth", which is unreferenced, out of the context, ambiguous (if not completely wrong) and unfocused (it is about provability and truth, not about proofs and knowledge). This is a very fragile premise to start with.
#3075
"You repeated this many times, but it's plainly false." ++ It is not. That is what you say. Prove.
"Several posters have proven or disproven concepts and provided references."
++ Like what? So far none have proven or disproven anything let alone provided references.
Most exclaim like you "false", "flawed", "fallacies", "mistakes", "fragile" etc. and that is it.
"You did not prove your ideas because the "proofs" are flawed." ++ They are not. That is what you say. So I make a statement, provide proof and / or reference and you can just say it is flawed
"To start, you use a supposedly known but not proven game-theoretic value of the game (a draw)" ++ I even provided evidence for that.
A) Expert opinions of world champions
B) AlphaZero autoplay with reference paper high draw rate and more with more time and even if stalemate is a win
C) ICCF WC results: high draw rate, rising over the years, even with 7 men win claims allowed > 50 moves without capture or pawn move
D) TCEC results high draw rate even with imposed slightly unbalanced openings
E) Human world championship matches based on cloud engine preparation
"to "deduce" (after other fallacies and mistakes - ++ that is what you say, proof?) an error rate per move. Yes, that is right from AlphaZero autoplay follows an error rate per move
I thus have proven that 4 white candidate moves suffice at 17 s/move for 1 error in 10^20 positions
That is consistent with opening knowledge like the reference from AlphaZero I provided and also consistent with Carlsen saying in an interview he considers 3 candidate moves.
"I asked you to give a reference of a scientific work where the authors claim they know something which is not either proven, or at least never disproven by a history of experiments. You provided only a statement: "provability is a higher degree of truth", which is unreferenced" ++ I told you that is from a feature article in Scientific American around 1977. I do not have that issue any more.
"This is a very fragile premise to start with." ++ That is not a starting premise.
Starting premises are:
The count of legal positions by Tromp 10^44.
I proved none of the sampled positions are sensible i.e. can occur in a game with > 50% accuracy. Mainly because of the multiple underpromotions to pieces not previously captured, each such underpromotion being a blunder.
I presented the more relevant Gourion count of 10^37 and I pointed out that even the vast majority of these are not sensible, thus arriving at an estimate of 10^32 sensible positions.
I pointed out that the vast majority of these positions is not reachable in the course of the solving process and made reference to solving Losing Chess and Checkers. Thus I estimate 10^19 reachable positions.
I pointed out that of the reachable positions the majority is not relevant for weakly solving chess.
I gave examples of non relevant positions and pointed to a reference indicating that using chess knowledge is allowed in weakly solving chess.
I thus arrived at an estimate of 10^17 legal, sensible, reachable, and relevant positions.
I then pointed out that from this follows that 3 cloud engines can weakly solve chess in 5 years, like Sveshnikov predicted.
I also analysed ICCF WC results and pointed out 99% of the drawn games are already ideal games with optimal moves from both sides, i.e. perfect play. I thus pointed out we already have over 1000 ideal games with optimal moves i.e. perfect play.
I also showed that ICCF WC games end on average in 39 moves.
I also showed that the 50-moves rule is never invoked and thus can be disregarded.
Nobody has responded yet to the point that if you know three pieces checking a King at once is illegal -
you don't need 'retrograde analysis' to know that four or more pieces so checking is illegal too.
A kind of 'loud silence' in response to that one.
4 pieces checking - is 'illegal on the board'. No need to computer it to show it 'couldn't have got there.
Illegal on the board versus 'couldn't have got there'.
'Response' wouldn't include spamming about Sveshnikov and phony computer speed figures and cosmetic reductions in the number of digits in numbers of positions to be solved though.
Is there a 'real discussion' in the posts ?
Yes I think it exists.
Is it like 'Cherenkov radiation' and it has to be Discovered ?
"You repeated this many times, but it's plainly false." ++ It is not. That is what you say. Prove.
For example, I have provided proof and reference that about 10¹⁴ nodes have been searched to solve checkers, not 10⁷ like you repeated for many posts; I have also provided a paper that states clearly how the authors interpret van den Herik definition of "weak solution", while you didn't; MARattigan has showed the pathology in Stockfish. But I have not to convince you, only those who are interested in the topic, who are invited to read from the beginning.
"To start, you use a supposedly known but not proven game-theoretic value of the game (a draw)" ++ I even provided evidence for that.
Your "evidence" is not a proof, otherwise chess would be already ultra-weakly solved. Just your word that you read the statement "provability is a higher degree of truth" on Scientific American proves nothing, sorry.
That is not a starting premise.
All your idea to cut off lines at early stage of the search is based on the supposed error rate per move, which in turn is "deduced" from the supposed game value. The real "accuracy" (not that computed by engines or by you) will be known (i.e. by proof) only after the solution. If it was really known, the game would be already weakly solved. Again, you use "known" but not proven things to prove other things, so all your idea of "solution" is based on that unreferenced an ambiguous statement.
@haiaku
But I have not to convince you, only those who are interested in the topic, who are invited to read from the beginning.
Regardless of 'convince' - that post is good - and numerous other good posts you've made.
The real discussion does happen some of the time.
It is not undiscovered 'Cherenkov radiation'.
😁^✅ 👋 🎵🎸
Not only "could", pretty sure that has been done. I think all of Euclid has been mechanised. Here is a paper about mechanical verification of book I.
Interesting paper. (Only twelve to go.)