51
Tournaments and Events / Re: Dominion Team World Cup II (Results Only)
« on: January 19, 2015, 10:44:06 pm »
Netherlands - United States B
florrat - NickSorbello 3:3
florrat - NickSorbello 3:3
Show Posts
This section allows you to view all posts made by this member. Note that you can only see posts made in areas you currently have access to.
52
Other Games / Re: Prismata: Alpha Key Giveaway! (Magic-Chess-Dominion-Starcraft hybrid game)
« on: January 19, 2015, 08:37:28 pm »
I got mine today. So yeah, they're still being handed out.
Thank you so much prismata devs!
Thank you so much prismata devs!
53
Dominion League / Re: Standings & Results
« on: January 16, 2015, 01:52:39 pm »
B1: Mr Anderson - florrat: 3 - 3
54
Dominion League / Re: Standings & Results
« on: January 16, 2015, 11:26:06 am »
B1: QwertZuiop - florrat: 3 - 3
55
Dominion League / Re: Standings & Results
« on: January 14, 2015, 06:19:03 pm »
B1, Fergesser - florrat: 3 - 3
56
Other Games / Re: Prismata: Alpha Key Giveaway! (Magic-Chess-Dominion-Starcraft hybrid game)
« on: January 13, 2015, 04:26:50 pm »
I'd love to get a key
57
Dominion General Discussion / Re: Possessed
« on: January 10, 2015, 10:05:58 pm »
And I thought this would be another topic whining about Possession.
59
Puzzles and Challenges / Re: Easy Puzzles
« on: January 06, 2015, 05:56:17 pm »
About ending the game in 2 turns: you can empty the supply in a game where 3 players have 2 turns each. I'm (over) halfway done with writing down a full solution, which I was planning to post it in this thread. If anyone is interested, I can post my incomplete solution, I'm not likely to complete it anytime soon. (I'm certain that it can be completed, the only question is with how much points player 3 can end, probably well over 1000).
60
Dominion League / Re: Standings & Results
« on: January 03, 2015, 12:19:13 pm »
B1, Monsieur X - florrat: 4 - 2
61
Dominion League / Re: Standings & Results
« on: December 31, 2014, 09:59:34 am »
B1: SheCantSayNo - florrat: 3 - 3
62
Dominion League / Re: timezones
« on: December 13, 2014, 07:40:48 am »
name: florrat
timezone: America/New_York
timezone: America/New_York
63
General Discussion / Re: Maths thread.
« on: November 30, 2014, 05:41:20 pm »
Yes, the Four Colour Theorem is also an impressive result that has been formally proven in a proof assistant.
I'm afraid that currently, you'll have no chance to give a proof in a proof assistant in similar time to giving it on paper. The problem is just that you have to give much more detail in the proof assistant. You can call some automated procedures for some basic steps, but it doesn't come near the steps mathematicians leave out in written proofs. To give you a rough idea about which level of detail is required, see for example this proof that the square root of 2 is not rational.
Still, it would be a pretty cool idea. It would be already feasible to do now, but currently you'll be mostly checking how well someone can formalize proofs in a proof assistant, rather than how well someone can come up with the proofs in the first place.
I'm afraid that currently, you'll have no chance to give a proof in a proof assistant in similar time to giving it on paper. The problem is just that you have to give much more detail in the proof assistant. You can call some automated procedures for some basic steps, but it doesn't come near the steps mathematicians leave out in written proofs. To give you a rough idea about which level of detail is required, see for example this proof that the square root of 2 is not rational.
Still, it would be a pretty cool idea. It would be already feasible to do now, but currently you'll be mostly checking how well someone can formalize proofs in a proof assistant, rather than how well someone can come up with the proofs in the first place.
64
Tournaments and Events / Re: Dominion Team World Cup II Signups
« on: November 30, 2014, 05:04:30 pm »
florrat
the Netherlands
all
the Netherlands
all
65
Dominion General Discussion / Re: Best Dominion Moments 2014
« on: November 30, 2014, 01:36:54 am »
It would be even better to draw Doctor during clean-up.
66
General Discussion / Re: Maths thread.
« on: November 30, 2014, 01:06:30 am »http://en.wikipedia.org/wiki/Higher-order_logicBut is proof checking undecidable in higher order logic? I tried to google it, but didn't find anything meaningful. The only thing the wikipedia article states about undecidability is about higher order unification, which is not needed to check a fully annotated proof.
My point is precisely that most mathematicians (barring those working in logic) do not. They usually do things like "let f be a function" or "consider the smallest subset such that", and those are second-order logic statements.
First order is extremely weak, you cannot even define the natural numbers or the real numbers with it.In set theory (in particular first order ZFC) all these statements can be expressed in first order logic. "f is a function from A to B" can be defined as "f is a subset of the cartesian product A * B and for all a in A there is a unique b in B such that the ordered pair (a,b) is in f." All these notions themselves can be also defined until you only have elementhood as primitive notion (and of course the logical notions (connectives and quantifiers)). After this, you can use this to quantify over functions, and similarly for subsets. And (of course) you can define the real numbers and natural numbers in set theory.
I guess this is kind-of answered above. I think the problem is unfeasible hard even for computer/human teams.Well, if you allow humans, this already happens today. Proofs are provided by a human to a computer program called a proof assistant, which can then fill in the remaining gaps, and produce a formal proof. This is called interactive theorem proving, and I'm currently doing a PhD related to this :-) It currently is much more work to write down a proof which will be accepted by the proof assistant than it is to write a proof on paper (hopefully this will change in the future).
However, many impressive results have already been formally proved this way. Perhaps most notably the Kepler conjecture, which asks what is the densest way to place spheres in space. This problem has been open for almost 400 years, until Thomas Hales claimed he found a proof in 1998. However, this proof was so complicated (and involved a lot of calculations performed by a computer) that it could not be verified by other mathematicians. Since then Hales has worked on a formalization in a proof assistant, which he completed this summer.
These proof assistants can output a formal proof. Usually those logical systems are more complicated than just first (or higher) order logic (allowing things like definitions or inductively defined structures), but it is definitely a logical system you can write down in a couple of pages, and which has decidable proof checking.
I just think that people are too eager for an all-encompassing theory of things that they will praise anything that sounds like it may be it. I believe such a thing does not exist, and moreover, we are getting far away from it. And I don't think there is a problem with that. Gödel, man. Same thing will likely happen at every level.Yeah, people tend to advocate too much for they like or belief in, including mathematical foundations. I also don't think there is a unique "best" foundation.
67
General Discussion / Re: Random Stuff Part II
« on: November 28, 2014, 06:34:26 pm »
Let's move this discussion over to the math(s) thread. It is statistically unlikely that there's so much advanced math in this thread.
68
General Discussion / Re: Maths thread.
« on: November 28, 2014, 06:34:07 pm »
(continued from discussion in random stuff thread)
I think most mathematician have faith that both their theorems and their proofs can be encoded in - for example - ZFC in classical first order logic, which is AFAIK the most accepted foundation of mathematics under mathematicians. Checking a formal proof in this logic is super decidable (I think linear in the length of the proof). Higher-order logics (intuitionistic or not) can also be decidable, such as the intentional Martin-Löf type theory. True, extensional type theory is undecidable, but I'm claiming that mathematicians rarely work specifically in extensional type theory (if only because they don't specify in which logic they work, and hence their informal proof can be formalized in many logics, some of which are decidable).
Or are you talking about another problem: translating mathematical proofs on paper accepted by other mathematicians to rigorous formal proofs in some (decidable) logic? I agree that such a translation is infeasibly hard, but I think this problem is too vague to say that it is undecidable. I think that if a proof contains enough details, it should be possible to translate it into a formal proof. This is what happens with proof assistants all the time.
And yes, in the end, a general theory is not strictly better, so a more general and a less general theory are incomparable, but I think the more general theory is better in 9 out of 10 aspects.
Mathematicians rarely prove things in a logic where proof-checking is decidable. They prove things in some form of intuitionisitic logic, usually with higher-order functions. SOME (possibly most, but I don't know) of those proofs COULD be translated into a proof in a logical system with computable proof-checking available, but (almost) nobody does it. And few people care enough to even have a sentence that says "this proof can *clearly* be made using this amount of logical power, so, we are cool".Can you elaborate what you mean with the first sentence? Can you give a specific undecidable logic where you think mathematicians work in?
I think most mathematician have faith that both their theorems and their proofs can be encoded in - for example - ZFC in classical first order logic, which is AFAIK the most accepted foundation of mathematics under mathematicians. Checking a formal proof in this logic is super decidable (I think linear in the length of the proof). Higher-order logics (intuitionistic or not) can also be decidable, such as the intentional Martin-Löf type theory. True, extensional type theory is undecidable, but I'm claiming that mathematicians rarely work specifically in extensional type theory (if only because they don't specify in which logic they work, and hence their informal proof can be formalized in many logics, some of which are decidable).
Or are you talking about another problem: translating mathematical proofs on paper accepted by other mathematicians to rigorous formal proofs in some (decidable) logic? I agree that such a translation is infeasibly hard, but I think this problem is too vague to say that it is undecidable. I think that if a proof contains enough details, it should be possible to translate it into a formal proof. This is what happens with proof assistants all the time.
There is some value in the generalization, of course, which is mostly connecting things that were seemingly disconnected. My point is that there is also a loss in value because the proof done directly on the subject at hand is much more illustrating on the phenomena the person reading the theorem is interested in. So, my point is not that category theory is useless (although I think category theory is a drug at this point, kind of like string theory for mathematicians), but that it is over-praised as the ultimate tool and even the only thing that is worthy (or legit...).I agree that a simple elementary proofs has a lot of merits. However, I do prefer a simple general proofs over complicated elementary proofs. And it is pretty common that a proof becomes simpler in a general setting. For example in category theory, there's often just one thing you can do in a proof, which makes proofs not that hard to find. More specifically about category theory: I'm neither saying that it is "the ultimate tool" or that it's the only worthy thing. However, I do think it's a very useful and very important tool. You might be interested in this (short) answer on stackexchange which gives examples where category theory has been useful for other fields of mathematics.
So, to come back to my original post, more general is not always better. I agree with you that it is sometimes better and I would add that it is usually incomparable.
Caveat + example: My very first paper on my PhD topic is a simple combinatorial proof of a fact that was already known, but required to combine more general results from three different papers. Doing that lead to the ability to produce results for similar scenarios which an author of one of those papers was unable to get despite working in the question for some time.
And yes, in the end, a general theory is not strictly better, so a more general and a less general theory are incomparable, but I think the more general theory is better in 9 out of 10 aspects.
69
General Discussion / Re: Random Stuff Part II
« on: November 27, 2014, 02:11:04 pm »
I agree with your general sentiment that math is a science. You might not be experimenting which things are true, but you are experimenting with which things are most useful, natural and general. However, I disagree on some points you make
I see your point that proofs "need to resonate with something within your head" and I agree with that. But when you're getting more and more used to a new general theory, I think that also happens in the general theory. If you're just learning it, you should just look what the things you're proving mean in examples.
Given that in modern mathematics most proofs are non-decidable and use higher-order logics, their correctness (i.e., the "truth" notion in math) is based on consensus.Wait, that's not a given. I think no mathematician works in logical frameworks where proof checking is undecidable (except for some logicians working in exotic logics, if you want to call them mathematicians (which I typically do)). Given a potential formal proof, there is a total algorithm checking that it is a correct proof. Of course, that it different from saying that provability is decidable: in most logics it is indeed the case that given a statement, it is undecidable to check whether the statement is provable.
It is not true that more general is always better: sometimes, generalizing too much makes the proofs lose focus on the meaning and just become manipulation of symbols. That is not the good math. Good math uses proofs to assign meaning / purpose to its definitions. For that to happen, the proofs need to resonate with something within your head that is not quantifiable. They need to be "natural". They need to "feel ok".I think if you generalized some topic so far that you can prove deep results just by manipulating symbols, you're doing something really well. I'm now mainly thinking about category theory, which is awesomely general. And the fact that it is so general, leads to new interesting discoveries. The "symbol manipulation" proof in category can be the essence of different proofs in different fields, and because you work in the general theory of categories, you see the connection between these different proofs or techniques in different fields, which itself is a useful insight.
I see your point that proofs "need to resonate with something within your head" and I agree with that. But when you're getting more and more used to a new general theory, I think that also happens in the general theory. If you're just learning it, you should just look what the things you're proving mean in examples.
70
Dominion League / Re: Standings & Results
« on: November 23, 2014, 04:55:38 pm »
B1: liopoil - florrat, 4 - 2
71
Dominion League / Re: Season 4 - Announcing livestreams
« on: November 23, 2014, 02:05:21 pm »
You're right. I forgot that 2 people demote.
72
Dominion League / Re: Season 4 - Announcing livestreams
« on: November 23, 2014, 01:57:01 pm »I'll be going live soon against florrat. One of us will demote (I need 4.5 to avoid demotion), and florrat has a chance to promote with 3 or more.Good point. I didn't see that I could still demote. All scores are so close to each other in our group! I just need 1 point to avoid demotion, though.
73
Rules Questions / Re: Bunch of Duration Questions
« on: November 20, 2014, 12:28:54 am »
So Sudgy, will your program be the first one to handle Outpost correctly? 
74
General Discussion / Re: A reference for f.ds lexicon and inside jokes
« on: November 20, 2014, 12:27:29 am »I demand satisfaction!Here you go: https://getsatisfaction.com/goko
75
Dominion League / Re: Standings & Results
« on: November 19, 2014, 02:19:30 pm »
B1: 2.71828... - florrat: 3 - 3