Dominion Strategy Forum

Please login or register.

Login with username, password and session length
Pages: 1 ... 6 7 [8] 9 10 ... 47  All

Author Topic: Maths thread.  (Read 306175 times)

0 Members and 1 Guest are viewing this topic.

florrat

  • Minion
  • *****
  • Offline Offline
  • Posts: 542
  • Shuffle iT Username: florrat
  • Respect: +748
    • View Profile
Re: Maths thread.
« Reply #175 on: June 29, 2014, 02:39:56 pm »
0

That's a good point, I stand corrected.
Logged

heron

  • Saboteur
  • *****
  • Offline Offline
  • Posts: 1055
  • Shuffle iT Username: heron
  • Respect: +1183
    • View Profile
Re: Maths thread.
« Reply #176 on: July 08, 2014, 11:58:51 pm »
0

Well, the problems for day 1 of the international mathematical olympiad are released today. http://www.artofproblemsolving.com/Forum/resources.php?c=1&cid=16&year=2014&sid=e94cbd1547c0c955ad8ef37cf50e71a0

I solved #1 and #2 (with some help from friends) in just under 2 hours, and am reasonably sure that I could solve #3 with complex numbers in the remaining 150 minutes if I were actually participating in the IMO, but it did not sound very fun to do for practice. I guess I will try to see if I can bash out that solution tomorrow.

I think that the problems are relatively easy for the IMO though, especially #2. What do you guys think?
Logged

SirPeebles

  • Cartographer
  • *****
  • Offline Offline
  • Posts: 3249
  • Respect: +5459
    • View Profile
Re: Maths thread.
« Reply #177 on: July 29, 2014, 03:02:29 pm »
+13

Logged
Well you *do* need a signature...

Kirian

  • Adventurer
  • ******
  • Offline Offline
  • Posts: 7096
  • Shuffle iT Username: Kirian
  • An Unbalanced Equation
  • Respect: +9411
    • View Profile
Re: Maths thread.
« Reply #178 on: July 29, 2014, 03:30:51 pm »
+3

...because they're uncountable?
Logged
Kirian's Law of f.DS jokes:  Any sufficiently unexplained joke is indistinguishable from serious conversation.

Joseph2302

  • Jester
  • *****
  • Offline Offline
  • Posts: 858
  • Shuffle iT Username: Joseph2302
  • "Better to be lucky than good"
  • Respect: +575
    • View Profile
Re: Maths thread.
« Reply #179 on: September 26, 2014, 12:37:15 pm »
0

I reckon P=NP, would be so cool if it did.
Logged
Mafia Stats: (correct as of 2017)
Town: 22 games, 8 wins
Scum: 5 games, 3 wins

florrat

  • Minion
  • *****
  • Offline Offline
  • Posts: 542
  • Shuffle iT Username: florrat
  • Respect: +748
    • View Profile
Re: Maths thread.
« Reply #180 on: November 28, 2014, 06:34:07 pm »
+1

(continued from discussion in random stuff thread)
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...).

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

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

soulnet

  • Mountebank
  • *****
  • Offline Offline
  • Posts: 2142
  • Respect: +1751
    • View Profile
Re: Maths thread.
« Reply #181 on: November 29, 2014, 12:41:01 pm »
+1

Can you elaborate what you mean with the first sentence? Can you give a specific undecidable logic where you think mathematicians work in?
http://en.wikipedia.org/wiki/Higher-order_logic

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.
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. And in category theory it is probably worse, as you are constantly using functions as the domain of functions, which takes you to third-order already, and then you are done with full-decidability.

First order is extremely weak, you cannot even define the natural numbers or the real numbers with it.

One possible thing is that all the proofs that use higher-order logic can be translated into weaker logics. That seems completely plausible to me. However, it would be extremely difficult to do, and quite likely, a waste of time. I don't care that math works by consensus, I actually like that it behaves like this, I like math being a science.

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

Any FOL with finitely many symbols is decidable. I never thought about linearity, but I guess you are probably right (if you count as "length of the proof" the sum of the lengths of each step). However, the size of a formal proof in an extension of a formal system like SP is probably enormous compared with the actual proof people write in a paper using a mixture of higher-order symbols (like functions) and natural language. Any quantification I can make here is no better than a wild guess, but if someone proofs that actual theorems can be proof with manageable-size proofs in a formal decidable system I would be amazed.

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.

I guess this is kind-of answered above. I think the problem is unfeasible hard even for computer/human teams.

You might be interested in this (short) answer on stackexchange which gives examples where category theory has been useful for other fields of mathematics.

I may get to read that eventually. I have some grasp on category theory: my best friend and two other friends did their masters' thesis on it, and two of them are currently finishing their PhDs on it as well. I was never too impressed I am afraid. That being said, with the current immense subdivision of fields of math, is hard to be really impressed by anything in which you are not an expert, so that's not really a meaningful statement. I am not claiming that category theory is worthless, 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.

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.

I probably disagree with you in which constitutes an "aspect".
Logged

florrat

  • Minion
  • *****
  • Offline Offline
  • Posts: 542
  • Shuffle iT Username: florrat
  • Respect: +748
    • View Profile
Re: Maths thread.
« Reply #182 on: November 30, 2014, 01:06:30 am »
+3

http://en.wikipedia.org/wiki/Higher-order_logic
But 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.
Logged

qmech

  • Torturer
  • *****
  • Offline Offline
  • Posts: 1918
  • Shuffle iT Username: qmech
  • What year is it?
  • Respect: +2320
    • View Profile
Re: Maths thread.
« Reply #183 on: November 30, 2014, 05:04:28 am »
+3

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 a PhD student.

is how I expected this to go.

Logged

blueblimp

  • Margrave
  • *****
  • Offline Offline
  • Posts: 2849
  • Respect: +1559
    • View Profile
Re: Maths thread.
« Reply #184 on: November 30, 2014, 10:11:47 am »
0

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.
Cool. I knew of formal proof methods being applied to the Four Colour Theorem, which states that any planar graph may have its faces coloured with four colors such that no two adjacent faces have the same colour. That is a similar situation in that the theorem was reduced to a bunch of computational case checking.

Here's a crazy idea I had related to proof assistants. There are many online programming contests, such as Topcoder, where you're asked to write program solving some algorithmic problem. An analogous competition wouldn't be feasible for math proofs, because the solutions require human judging, which would be impractical at that scale. An automated proof checker could fix that problem by allowing automated checking of the proofs, at the cost of requiring competitors to write formal proofs.

My question is whether there's a formal proof system that would be appropriate for that application. The main requirement would be that formalizing the proof, once you're familiar with the proof system, needs to be significantly easier than thinking of the informal proof in the first place. For example, ideally an hour or so would be enough for a skilled competitor to solve and formalize a problem of difficulty comparable to an easy Putnam problem. Is there any system capable of that today?
Logged

florrat

  • Minion
  • *****
  • Offline Offline
  • Posts: 542
  • Shuffle iT Username: florrat
  • Respect: +748
    • View Profile
Re: Maths thread.
« Reply #185 on: November 30, 2014, 05:41:20 pm »
+1

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

Trogdor the Burninator

  • Golem
  • ****
  • Offline Offline
  • Posts: 176
  • Respect: +76
    • View Profile
Re: Maths thread.
« Reply #186 on: November 30, 2014, 08:50:47 pm »
+1

How did the constipated mathematician solve his problem?
He worked it out with a pencil...

Logged
Dominion.games username: Jolinar of Malkshur





https://www.youtube.com/watch?v=VHF_bIjIPAE

(I did not create the Trogdor the Burninator song nor am I associated with its producers in any way.  I just think it sounds cool. :P)

AndrewisFTTW

  • Saboteur
  • *****
  • Offline Offline
  • Posts: 1129
  • Respect: +1084
    • View Profile
Re: Maths thread.
« Reply #187 on: December 01, 2014, 02:39:26 pm »
+2

How did the constipated mathematician solve his problem?
He worked it out with a pencil...

Where's the "unsubscribe" button?
Logged
Wins: M39, M41, M48, M96, M97, M102, M105
Losses: M40, M43, M45, BM17 (?), RMM13, RMM17, RMM20, NM7, ZM18, M100, M109
MVPs: M97
Mod/Co-Mod: M46, M49, M52, NM10

Trogdor the Burninator

  • Golem
  • ****
  • Offline Offline
  • Posts: 176
  • Respect: +76
    • View Profile
Re: Maths thread.
« Reply #188 on: December 03, 2014, 11:39:35 am »
+1

How did the constipated mathematician solve his problem?
He worked it out with a pencil...

Where's the "unsubscribe" button?

Mwa ha ha! Trogdor strikes again!!
Logged
Dominion.games username: Jolinar of Malkshur





https://www.youtube.com/watch?v=VHF_bIjIPAE

(I did not create the Trogdor the Burninator song nor am I associated with its producers in any way.  I just think it sounds cool. :P)

sudgy

  • Cartographer
  • *****
  • Offline Offline
  • Posts: 3431
  • Shuffle iT Username: sudgy
  • It's pronounced "SOO-jee"
  • Respect: +2706
    • View Profile
Re: Maths thread.
« Reply #189 on: December 03, 2014, 05:12:33 pm »
0

I always feel amazing when I figure out some new (for me) math thing on my own...  I just realized that the derivative of the volume of a sphere is the surface area of the sphere...  I have no idea of the implications, but it's still really cool.
Logged
If you're wondering what my avatar is, watch this.

Check out my logic puzzle blog!

   Quote from: sudgy on June 31, 2011, 11:47:46 pm

liopoil

  • Margrave
  • *****
  • Offline Offline
  • Posts: 2587
  • Respect: +2479
    • View Profile
Re: Maths thread.
« Reply #190 on: December 03, 2014, 05:17:49 pm »
0

I always feel amazing when I figure out some new (for me) math thing on my own...  I just realized that the derivative of the volume of a sphere is the surface area of the sphere...  I have no idea of the implications, but it's still really cool.
That's true?

Let's see.... 4/3 pi r^3.... 4 pi r^2.

Is 4 pi r^2 the surface area of a sphere? I honestly don't know. If so, that is pretty cool.

Now that I think about it, the same is true for a circle; the derivative of pi r^2 is 2 pi r.

Is it true for an n-sphere? I don't know why you would ever take the derivative of a volume anyway though.
Logged

WalrusMcFishSr

  • Minion
  • *****
  • Offline Offline
  • Posts: 642
  • An enormous walrus the size of Antarctica
  • Respect: +1793
    • View Profile
Re: Maths thread.
« Reply #191 on: December 03, 2014, 05:19:55 pm »
+6

Yep...it makes perfect sense if you think about "growing" a sphere by stacking lots of thin shell "surface areas" on each other.
Logged
My Dominion videos: http://www.youtube.com/user/WalrusMcFishSr   <---Bet you can't click on that!

Kirian

  • Adventurer
  • ******
  • Offline Offline
  • Posts: 7096
  • Shuffle iT Username: Kirian
  • An Unbalanced Equation
  • Respect: +9411
    • View Profile
Re: Maths thread.
« Reply #192 on: December 03, 2014, 05:25:14 pm »
+4

I always feel amazing when I figure out some new (for me) math thing on my own...  I just realized that the derivative of the volume of a sphere is the surface area of the sphere...  I have no idea of the implications, but it's still really cool.
That's true?

Let's see.... 4/3 pi r^3.... 4 pi r^2.

Is 4 pi r^2 the surface area of a sphere? I honestly don't know. If so, that is pretty cool.

Now that I think about it, the same is true for a circle; the derivative of pi r^2 is 2 pi r.

Is it true for an n-sphere? I don't know why you would ever take the derivative of a volume anyway though.

The volume of an n-sphere is the integral from 0 to r of the surface area (concentric spherical shells).

So the answers are yes, and, you wouldn't, but you'd integrate the surface area.
Logged
Kirian's Law of f.DS jokes:  Any sufficiently unexplained joke is indistinguishable from serious conversation.

Kirian

  • Adventurer
  • ******
  • Offline Offline
  • Posts: 7096
  • Shuffle iT Username: Kirian
  • An Unbalanced Equation
  • Respect: +9411
    • View Profile
Re: Maths thread.
« Reply #193 on: December 03, 2014, 05:25:50 pm »
0

And, ninja'd.
Logged
Kirian's Law of f.DS jokes:  Any sufficiently unexplained joke is indistinguishable from serious conversation.

soulnet

  • Mountebank
  • *****
  • Offline Offline
  • Posts: 2142
  • Respect: +1751
    • View Profile
Re: Maths thread.
« Reply #194 on: December 03, 2014, 06:33:04 pm »
0

But 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.
I guess I always thought unification < proof checking because, you know, who fully annotates proofs? I guess fully annotated proof checking is always computable in a "reasonable" proof system, because that is a pretty good definition for the intuitive idea of a "reasonable" proof system.

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.
Maybe we have different ideas of what a "definition" entails. For me, if your definition accept non-standard models (i.e., models other than isomorphisms of the idea you have in your head), then, it is not a good definition. And I think any first order theory that includes the natural numbers always accepts non-standard models (and similarly for the reals).

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 did not know it was a common practice to "re-prove" things with proof assistants. I knew about the four color theorem case and I have heard recently of the Kepler conjecture in the "news", but not that it was widely done. I am still willing to bet it is only a negligible percentage of the theorems done (and with good reason).

I also don't think there is a unique "best" foundation.

How about this one?
Logged

qmech

  • Torturer
  • *****
  • Offline Offline
  • Posts: 1918
  • Shuffle iT Username: qmech
  • What year is it?
  • Respect: +2320
    • View Profile
Re: Maths thread.
« Reply #195 on: December 04, 2014, 04:06:58 am »
0

Maybe we have different ideas of what a "definition" entails. For me, if your definition accept non-standard models (i.e., models other than isomorphisms of the idea you have in your head), then, it is not a good definition. And I think any first order theory that includes the natural numbers always accepts non-standard models (and similarly for the reals).

Yes, that's Löwenheim–Skolem.  And I'm not sure how disturbing I find it.  At least everything you can prove about the natural numbers is true there.

I always feel amazing when I figure out some new (for me) math thing on my own...  I just realized that the derivative of the volume of a sphere is the surface area of the sphere...  I have no idea of the implications, but it's still really cool.

This hints at why the similarity of the notation ∂A for the boundary of a set A to a derivative is not entirely coincidental.
Logged

heron

  • Saboteur
  • *****
  • Offline Offline
  • Posts: 1055
  • Shuffle iT Username: heron
  • Respect: +1183
    • View Profile
Re: Maths thread.
« Reply #196 on: January 02, 2015, 08:28:27 pm »
0

Here's a classic problem:

What is the least prime factor of 63^128 + 1?
No cheating with computers please!

Edit: Um, made an error here. More difficult version found a few posts below.

« Last Edit: January 02, 2015, 09:57:03 pm by heron »
Logged

silverspawn

  • Adventurer
  • ******
  • Offline Offline
  • Posts: 5296
  • Shuffle iT Username: sty.silver
  • Respect: +3182
    • View Profile
Re: Maths thread.
« Reply #197 on: January 02, 2015, 09:14:43 pm »
+1

Here's a classic problem:

What is the least prime factor of 63^128 + 1?
No cheating with computers please!

Moat?

liopoil

  • Margrave
  • *****
  • Offline Offline
  • Posts: 2587
  • Respect: +2479
    • View Profile
Re: Maths thread.
« Reply #198 on: January 02, 2015, 09:26:09 pm »
+3

Here's a classic problem:

What is the least prime factor of 63^128 + 1?
No cheating with computers please!
Does this work?

63 = 7*3^2, so 63^128 + 1 = 7^128*3^256 + 1

The last digits of powers of 3 are 3, 9, 7, 1, repeat. 256 is divisible by 4 so the power of 3 term ends in 1.

The last digits of powers of 7 end in 7, 9, 3, 1, repeat. 128 is divisible by 4 so the power of 7 term ends in 1. Their product must also end in 1 then. Add one and the expression ends in 2. Therefore the number is divisible by 2, which is the smallest prime that there is. So the answer is 2.
Logged

heron

  • Saboteur
  • *****
  • Offline Offline
  • Posts: 1055
  • Shuffle iT Username: heron
  • Respect: +1183
    • View Profile
Re: Maths thread.
« Reply #199 on: January 02, 2015, 09:56:31 pm »
0

Oh whoops, made an error with the problem. Um, we'll call that easy mode. But yea, liopoil has it right.
Okay, hard mode:

What is the least prime factor of 252^128 + 1?
Logged
Pages: 1 ... 6 7 [8] 9 10 ... 47  All
 

Page created in 0.06 seconds with 21 queries.