If you're going to those lengths, you probably aren't just some random person who wants to stop his pr0n collection being discovered. Hammers do not reliably erase data; sure, the discs may be bent and the HD itself is never going to work again, but you'd still be able to get a competent disaster recovery specialist to get at least 90% of the data off the disc.
That said, if you're being paranoid then railway thermite (melts, doesn't explode) is cheap and very effective. Open the case, pour thermite powder in all round, use a mag ribbon to light it and no data will be coming off that disc.
In unix, you personally can run as root, this allows you to screw up (more easily than a windows admin in some ways). Your background tasks, however, should be running in dummy users. mySQL runs as mysql, for example, it cannot e.g. see files outside its/dbs. If someone runs an exploit against it, then they only get access to a very small part of my system, not including most of my data.
If on the other hand I try that with windows, then the mySQL exploit allows access to all my personal data straight away. I can't (easily) have mySQL running as a dummy user with minimal privileges.
That's not really relevant to 'you should not run as root', though, that's a built in security flaw with windows.
You, the person on the chair in front of the machine, can run as root without compromising security.
You lose all protection from your own fuckups, of course, and that includes being social-engineered into clicking on the interesting file someone emailed you. But no security compromise, assuming you know enough to recognise a crack attempt when you see one, so won't actively cooperate.
Why? Suppose I'm logged in as peter, and you try to hack my box via my mySQL installation. You need to hack mySQL, then you need to run an escalation exploit to get root access, then you have my box.
Now suppose I'm logged in as root, and you try to hack my box via my mySQL installation. You need to hack mySQL, then you need to run an escalation exploit to get root access, then you have my box.
Hey... I just wrote the same thing twice. Why did I do that? Maybe because mySQL does not run as root, whether or not I am logged in as root.
However 99% of UNIX users will not recognise a hack attempt when they see it, and will run the pretty file they got by email, or install the dodgy WaReZ. So 99% of UNIX users should not ever run as root because they can't be trusted. Then 9 out of 10 of the people who can be trusted prefer to be protected from their typoes in unfortunate places and only run as root when they need to. The 1 in 1000 people left over can be trusted to run as root and are confident that they won't accidentally rm-rf whatever. They can run as root, their box is no more likely to be owned than anyone else's.
There are something like a million papers published per year. Of those, maybe ten will later be found to be plain wrong, and another several hundred will have gaps which can't be easily filled. That's still less than a tenth of a percent. If I pick up some random paper I will probably find no errors in it. If I want to use results from it, I will read the proofs properly and check them anyway, because understanding the proof is often more helpful than understanding the result. But I will very seldom find myself wanting to use some result and discovering that the purported proof is not valid.
There are standards for a formal proof - the basic sequence of formal logic statements - and these allow you to construct a proof checker easily. The problem, as you say, is translating your proof into formal logic; this is not something that a practising mathematician will be willing to do. It would be thoroughly boring, it would take weeks, and during those weeks while I muck about with logic that only a computer will ever read, some other guy is publishing the same result in a journal that doesn't need this silly extra proof, or working on my next result.
It may become common to publish computer-checkable proofs with normal papers, but that will not happen until creating the computer-checkable proof does not take the mathematician significant extra time. Which will require a computer program that is a lot closer to genuine artificial intelligence than anything we have yet.
I don't see any good reason to routinely publish formal proofs (by which I assume you mean computer-checkable) as well as a proof such as is commonly published. Yes, it would allow any mathematician to check the proof was correct without having to spend time reading and understanding the proof. But that's supposed to be the job of the reviewer, and the reviewer is seldom wrong. Also, if you are doing a bit of maths where it would be useful to use a result in some paper, then you generally want to be able to understand why the result is true, so you want to read the paper and understand the proof: it's in the right area, chances are there are ideas you can use yourself as well as the final result. Secondly, formal proofs are not just a bit longer than proofs as normally published. To look at the example I provided - I claimed that the identification between homomorphisms was natural. I actually didn't even refer to 'natural' in the proof - why? Because it should be obvious on reading the proof that I haven't had to play choice games, like choosing a vector space basis, to get my result, so that makes the identification natural. But I haven't ever tried to refer to the category of Frechet algebras and find myself a natural map (or whatever the category theory term is, I forget, it's not interesting anyway) to actually prove that it's a natural identification. Doing that - just that, not the rest of the proof - in formal logic would probably take several pages.
Then, what do I mean by '$T$ is continuous at $0$'?
and that is a nice simple concept, easily expressed in formal logic. In fact, the whole proof is pretty simple stuff; you could read a bit of linear algebra, a bit of epsilon/delta analysis, and you'd know all you need to follow it.
So, yes, you could build up a library of formal proofs of statements. But it would be much larger than a library of informal proofs, and it would not be of much use.
I also don't see any justification for your last statement. Yes, some proofs give rise to useful algorithms, and to use the algorithm is roughly the same as writing the proof in formal logic. However, much as it may surprise you, mathematicians tend to notice those and give the algorithm in at least pseudo-code form in the paper. Most proofs don't give useful algorithms.
Mathematics _can be_ formalised. But no-one writes mathematics that way. First, because when a mathematician finds he has a proof the first thing on his mind is to publish ASAP to stop anyone else getting there first and taking all the credit, second because in practice writing in formal logic (or even mainly in formal logic) leads to long, boring, unclear proofs which do not enhance reputation the way a relatively short clear proof does. A boring proof is a sequence of equations and formal logic; this sort of thing is really only used when proving a little lemma that's almost obvious anyway. Most proofs will look something like the following (LaTeX) discussing a Frechet algebra F; B_n are the Banach algebras associated to the seminorms of F, the pi_n are projections from F to B_n, the d_n are the chain maps between the B_n:
\begin{lemma} We may naturally identify continuous homomorphisms to $\mathbb C$ from $F$ and from the $B_n$, and so write \[\Delta(F,\mathbb C)=\bigcup_{n=1}^{\infty}\Delta(B_n,\mathbb C)\] \end{lemma} \begin{proof} If $\theta:B_n\rightarrow \mathbb C$ is a continuous homomorphism then so is $\theta\circ d_n:B_{n+1}\rightarrow \mathbb C$. Since $d_n$ has dense range, different $\theta$ give different $\theta\circ d_n$ and we may identify $\theta$ with $\theta\circ d_n$. Since also $\pi_n$ has dense range, we may identify $\theta$ with $\theta\circ \pi_n$. This allows us to write \[\Delta(F)\supseteq\bigcup_{n=1}^{\infty}\ Delta(B _n)\]
and it remains only to show that there are no extra continuous homomorphisms. \\
Suppose then that $T$ is a continuous homomorphism from $F$ to $\mathbb C$. In particular, $T$ is continuous at $0$, i.e. there is an open neighbourhood $U$ of $0$ such that $|T|1$ on $U$. This set is open in the inverse limit topology, i.e. is the intersection of the inverse limit space and an open set in the cross product of the $B_n$ with the product topology. $U$ may be assumed to be a set in a basis for the topology, so that it is the intersection of the $\pi_j^{-1}(U_j)$ for some $U_j$ open in $B_j$, up to some finite n.
Since the $d_j$ are continuous, however, this intersection must contain $\pi_n^{-1}(V)$ for $V$ an open neighbourhood of 0 in $B_n$, the intersection of the inverse images of the $U_j$. \\
We now show that $T=\theta\circ \pi_n$ for some $\theta\in\Delta(B_n)$, i.e. that $T(a)$ depends only on $a_n$, or that if $a_n=0$ then $T(a)=0$: if $a_n=0$, then $ka_n=0$ for all $k$, so $ka \in \pi_n^{-1}(V)$, and $|T(ka)|1$, for all $k$. But then $|T(a)|=0$ as required. \end{proof}
That's a bit like saying that the obvious and most reliable way to measure the weight of an object is to atomise it, count all the atoms of each type, and add up. In other words, it works, it will give you the right answer, but it takes far too long to be of any practical use.
If you wrote out the proof of Fermat's Last Theorem in formal logic without leaving gaps, for example, you'd end up with a stack of pages several metres high.
Cunning clue here: if there is a problem which took mathematicians a century to prove true, and you think there is a trivial reason why it is false, then you are wrong. In this case, because you don't have to use all four colours with the states along the top.
A computer can prove any theorem, if you give it long enough.
Reason: a theorem is a statement which has a proof. A proof is a finite sequence of logical statements. You can order all sequences of logical statements by lexicographic order within the sum of the number of variables used and the number of statements; then simply have a computer run through all sequences of logical statements in that order, checking each one to see whether the statements in the sequence are either axioms or follow by the rules of logic from the axioms, and checking whether the final statement is the statement you want to have proved. The computer will eventually reach a proof of whatever theorem you asked it to prove. Note that if you asked it to prove a statement which is not a theorem, it will never stop. Goedel's theorem tells us that there are some statements where not only will the computer fail to prove the statement true, it will also never prove the statement false.
The problem with trying to do this in practice is that for any interesting problem the shortest proof might not fit in a telephone directory - and the computer would be trying to find it by checking through all sequences of that size. It would take far too long.
The theoretical problem you refer to is whether one can write a program which will correctly classify all statements as true or false - this is not possible; some statements are neither. If you allow it to classify as 'neither' as well, it is still not possible - the sketch above will never classify any statement as 'neither' because with such statements it never halts, for example. Turing proved that no program can correctly classify all statements.
You're thinking about chromatic number of a graph, where you colour edges of a graph.
However, when you colour regions (or countries, or however you want to look at it) then maybe this country is touching a million other countries, but I will be able to find a way of colouring all those other countries using only red, green and blue, and I will still be able to colour the whole map with only four colours.
(this has nothing really to do with real world geography maps, it just happens to be a nice way to visualise things)
It is very easy to produce a validator which correctly classifies valid and invalid proofs written in formal logic. It is very easy to prove that the validator does what it is meant to do.
We don't know whether this abstract formal logic thing actually has any resemblance to the real world - that is not Goedel's theorem, which assumes logic to be valid and discusses potentially interesting frameworks for mathematics. Whether formal logic 'works' is simply something you have to believe, you cannot argue it, for the obvious reason. Whether you can use formal logic to demonstrate that your mathematical axioms are consistent is not obvious; Goedel's theorem states that in fact whenever your mathematical axioms are strong enough to produce interesting mathematics, you cannot demonstrate consistency.
The reason why mathematicians do not like computer proofs (as much as normal proofs, anyway) and do not like computer validation (always) are:
Computer proofs tend not to give any insight into why a statement is true. They simply check vast numbers of cases, when there might exist a simple argument which gives understanding. However, there is usually interesting mathematics involved in reducing the original problem to something which can be computer checked.
It is not easy to produce a program which will verify a proof written by a normal person, in the same way that it is hard to write a program which can spot contradictions in any argument written in natural English.
An argument written out in formal logic, although easy to verify for a computer, is generally much, much longer than the same argument written by a normal person, and even if you wanted to read the telephone-directory sized proof, the interesting ideas are so dispersed that you would gain no understanding from the proof.
So, a computer verifier would only be useful when a proof is written in formal logic - which only a computer would do for a proof of any interesting statement. But the computer proof won't give a mathematician any understanding of why the statement is true, so the mathematician doesn't like it. Furthermore, because formal logic is so long-winded, it doesn't seem likely that a computer will ever be able to prove interesting statements by doing a simple bash out formal logic until it works approach. IMO, a computer program which can prove interesting mathematical statements in sensible amounts of time will be about as hard to write (and probably not too dissimilar to) a Turing-capable program.
It's technically possible, and actually quite easy, to build a detector that will tell you when a TV is operating nearby. You could build a detector that will find computers; stuff like the HDD give off a fairly unmistakable signal. But it would not be easy or cheap.
In any case, the 'detector vans' the TV licensing supposedly use are no more than a scare story. The TV licensing people simply go round and pester anyone who does not have a TV licence; they assume everyone has a TV.
This new tax idea isn't supposed to happen before 2017, by which time supposedly TV will not be RF broadcast as it is now, but transmitted over broadband lines which will also be used for Internet access etc. So chances are they will decide that what actually should be taxed is the broadband connection itself, not the PCs.
Basically, you can look at light, or electrons, or whatever, as either a particle or a wave. Sometimes one interpretation will work better (light as a particle explains the photoelectric effect, light as a wave explains interference patterns, diffraction, etc). Current state of play is that the wave interpretation is always the best way to look at things, except when you observe the system everything collapses to particles, and when something mathematically inconvenient happens (you can explain the photoelectric effect in terms of waves, but the maths is horrible).
Classic two slit experiment with light consists of shining laser light on a barrier with two slits; each slit produces a diffraction pattern (http://en.wikipedia.org/wiki/Diffraction), the diffraction patterns interfere to produce the classic two slit pattern, see same link. This basically works because the laser light is coherent, you can (sort of) treat all the photons coming from the laser like one photon.
If you do this with electrons, because electrons are waves, you get the same patterns. Ditto any other particle.
Even if you do this experiment firing only one electron at a time you will get the same two-slit interference pattern, although 'common sense' tells you the electron can only pass through one of the two slits what actually happens is it passes through both at once. If on the other hand you fit a detector over one slit to register the passage of electrons, so you can tell which slit the electron passes through, you lose the interference pattern, you get two overlapping single slit diffraction patterns, which is not the same thing.
Roughly, if you have two slits and whenever an electron is fired at the slits you do not know which slit it went through, but the classical probability (what you'd expect if you didn't know quantum mechanics) of either slit is 0.5, then you will get a two-slit pattern.
This is basically the same experiment, except instead of two slits in space a little distance apart there are two possible source times for the electron, separated by a small time gap. There is no way to know whether a detected electron was produced at the first or second time, so the maths works out (roughly) the same as for the two slits in space case and you would expect to see the classic two-slits pattern. But it is kind of neat that someone's actually found a way to test that idea.
Why bother constructing a phony reader? Just buy one of VISA's standard ones, and stick a bit of software on it that charges $24.99 every time it can find a card in range.
Of course, the problem here is that when a thousand complaints come in to VISA HQ from people asking what the hell this charge is for, VISA take about three seconds to see that all the complaints refer to your merchant account and you get jailed. A phony reader or whatever makes no difference here - you may be able to fake out the card, but to get money you have to give VISA an account number to transfer money from and your account to transfer money to. And that is enough for VISA to catch you when complaints come in.
Offhand, the only immediately obvious way you can safely make money out of this is to make yourself a broadcast and amplify kit, which you can scan for your $20 of shopping at the supermarket, and hope that someone else (like the next guy in the queue) is near enough to you that his card activates and pays for you. Even that would be both very hard to do (magnetic induction powering a card a few feet away would be pretty hard to manage).
First, because scheduling everything is much easier when you only have to worry about one clock speed (or at least, only a few multiples of one clock speed).
Second, because once you've set up a production process which can fab latest and greatest processor on one half of the die, it's really not much more expensive to fab a second latest-and-greatest on the other half than a four years old core. It's not two chips, it's one chip which has two processors on it.
I'd point out that in fact pattern recognition is a major component to chess play. But because the patterns are so simple, all the pattern recognition is done in the first second or so of your turn. The rest of the turn is analytic thinking. Good example of this is when you play 1 or 2 minute chess - you never have time to think about it, all your time is spent recognising patterns and responding. You can get in about 1 move a second like that, but the level of game play only drops to what you'd expect in a normal game between players ranked about 100-150 points lower.
Whereas with go (note: my play is poor) you can only get away with auto-responding to patterns when you're in a very restricted situation; trying it when you're playing in a large area will lose you the game.
UK law would have Lindows lose that case, anyway: it's a name designed to have a similar sound to the MS trademark and competing with said MS product. IOW, calling it 'Lindows' was a stupid idea in the first place.
Whereas MAME existed way before Ultracade, so per UK law Ultracade would lose its trademark on 'MAME' as soon as MAME objected.
To some extent, even if a savant was producing poly-time solutions, it might not indicate that they were using a better algorithm.
NP-complete essentially means a problem which is as hard as possible given you can check the solution is right in polynomial time. It follows that an infinitely parallel computer (e.g. a quantum computer) can solve all NP problems in polynomial time; if a savant were essentially acting as a massively parallel computer then your experiment might return a polynomial time solution simply because you never tested the savant with large enough problem sizes to stop them being run in parallel.
He pretty much taught himself maths out of a exam-cramming textbook. Result being that he didn't know what a formal proof was until he came to England, and he never had any interest in repeating himself and going over the logic again. He produced proofs himself for some theorems, and left enough clues for other people (Hardy) to reconstruct his proofs for the rest of his theorems. Then there are a fair number of conjectures, some of which Ramanujan said he'd solved, most of which he didn't.
And in fact forming a useful conjecture is not easy. It's not hard to form an incredibly difficult conjecture which no-one solves for many years, it is hard to form a conjecture which you might reasonably expect to be able to solve.
By the way, FLT was called that because Fermat left behind a lot of statements which he claimed to be true. Most of them he had written solutions for, although usually not actually attached to the statement (he tended to demonstrate his cleverness by solving problems other people put up, some general proofs were found in these solutions). Some of them were proved true by other mathematicians after Fermat's death, no-one knows whether Fermat ever had a proof. A few of them were plain wrong (such as a conjectured formula which always took prime values - it didn't). But because these conjectures often were in fact true, and fairly frequently the mathematician who found a proof discovered that the same logic could be found elsewhere in Fermat's works, so that Fermat probably had in fact had a proof, there was a tendency to label all of those conjectures as theorems requiring proof. The Last Theorem was the one left over after all the others had been settled.
Yes, but there are interesting things in maths and there are less interesting things.
A table of all primes up to N is very interesting, lots of things to see.
A general theorem is usually interesting.
Spending a long time finding Mersenne primes is boring. We already know just about everything we want to know about Mersenne primes; the only major open question is whether there exist infinitely many, and that can't be answered by searching. A long string of 1s is not interesting, even when there are a prime number of 1s, and even when the binary number given by that string is itself prime. It's interesting that such things exist, and that there are nice algorithms for primality, but we already know that.
> Yes, and no single program can use an > infinite amount of space. So, if you > are given an arbirtary program that will > produce an output then you can compute that > output using only finite memory.
But you do not (in general) know how much memory will be used until after you've run the program - if you have N amount of memory and attempt to run the program then almost surely you will fail, for any given N.
I think we've got to about the same place in this argument, though:-)
Slashdot Mirror
If you're going to those lengths, you probably aren't just some random person who wants to stop his pr0n collection being discovered. Hammers do not reliably erase data; sure, the discs may be bent and the HD itself is never going to work again, but you'd still be able to get a competent disaster recovery specialist to get at least 90% of the data off the disc.
That said, if you're being paranoid then railway thermite (melts, doesn't explode) is cheap and very effective. Open the case, pour thermite powder in all round, use a mag ribbon to light it and no data will be coming off that disc.
Major difference between unix and windows.
/dbs. If someone runs an exploit against it, then they only get access to a very small part of my system, not including most of my data.
In unix, you personally can run as root, this allows you to screw up (more easily than a windows admin in some ways). Your background tasks, however, should be running in dummy users. mySQL runs as mysql, for example, it cannot e.g. see files outside its
If on the other hand I try that with windows, then the mySQL exploit allows access to all my personal data straight away. I can't (easily) have mySQL running as a dummy user with minimal privileges.
That's not really relevant to 'you should not run as root', though, that's a built in security flaw with windows.
You, the person on the chair in front of the machine, can run as root without compromising security.
You lose all protection from your own fuckups, of course, and that includes being social-engineered into clicking on the interesting file someone emailed you. But no security compromise, assuming you know enough to recognise a crack attempt when you see one, so won't actively cooperate.
Why? Suppose I'm logged in as peter, and you try to hack my box via my mySQL installation. You need to hack mySQL, then you need to run an escalation exploit to get root access, then you have my box.
Now suppose I'm logged in as root, and you try to hack my box via my mySQL installation. You need to hack mySQL, then you need to run an escalation exploit to get root access, then you have my box.
Hey... I just wrote the same thing twice. Why did I do that? Maybe because mySQL does not run as root, whether or not I am logged in as root.
However 99% of UNIX users will not recognise a hack attempt when they see it, and will run the pretty file they got by email, or install the dodgy WaReZ. So 99% of UNIX users should not ever run as root because they can't be trusted. Then 9 out of 10 of the people who can be trusted prefer to be protected from their typoes in unfortunate places and only run as root when they need to. The 1 in 1000 people left over can be trusted to run as root and are confident that they won't accidentally rm-rf whatever. They can run as root, their box is no more likely to be owned than anyone else's.
There are something like a million papers published per year. Of those, maybe ten will later be found to be plain wrong, and another several hundred will have gaps which can't be easily filled. That's still less than a tenth of a percent. If I pick up some random paper I will probably find no errors in it. If I want to use results from it, I will read the proofs properly and check them anyway, because understanding the proof is often more helpful than understanding the result. But I will very seldom find myself wanting to use some result and discovering that the purported proof is not valid.
There are standards for a formal proof - the basic sequence of formal logic statements - and these allow you to construct a proof checker easily. The problem, as you say, is translating your proof into formal logic; this is not something that a practising mathematician will be willing to do. It would be thoroughly boring, it would take weeks, and during those weeks while I muck about with logic that only a computer will ever read, some other guy is publishing the same result in a journal that doesn't need this silly extra proof, or working on my next result.
It may become common to publish computer-checkable proofs with normal papers, but that will not happen until creating the computer-checkable proof does not take the mathematician significant extra time. Which will require a computer program that is a lot closer to genuine artificial intelligence than anything we have yet.
I don't see any good reason to routinely publish formal proofs (by which I assume you mean computer-checkable) as well as a proof such as is commonly published. Yes, it would allow any mathematician to check the proof was correct without having to spend time reading and understanding the proof. But that's supposed to be the job of the reviewer, and the reviewer is seldom wrong. Also, if you are doing a bit of maths where it would be useful to use a result in some paper, then you generally want to be able to understand why the result is true, so you want to read the paper and understand the proof: it's in the right area, chances are there are ideas you can use yourself as well as the final result. Secondly, formal proofs are not just a bit longer than proofs as normally published. To look at the example I provided - I claimed that the identification between homomorphisms was natural. I actually didn't even refer to 'natural' in the proof - why? Because it should be obvious on reading the proof that I haven't had to play choice games, like choosing a vector space basis, to get my result, so that makes the identification natural. But I haven't ever tried to refer to the category of Frechet algebras and find myself a natural map (or whatever the category theory term is, I forget, it's not interesting anyway) to actually prove that it's a natural identification. Doing that - just that, not the rest of the proof - in formal logic would probably take several pages.
Then, what do I mean by '$T$ is continuous at $0$'?
Well:
$\forall \epsilon > 0, (\exists \delta>0: (\forall x\in $F$, |x|\delta) |T(x)|\epsilon )$
and that is a nice simple concept, easily expressed in formal logic. In fact, the whole proof is pretty simple stuff; you could read a bit of linear algebra, a bit of epsilon/delta analysis, and you'd know all you need to follow it.
So, yes, you could build up a library of formal proofs of statements. But it would be much larger than a library of informal proofs, and it would not be of much use.
I also don't see any justification for your last statement. Yes, some proofs give rise to useful algorithms, and to use the algorithm is roughly the same as writing the proof in formal logic. However, much as it may surprise you, mathematicians tend to notice those and give the algorithm in at least pseudo-code form in the paper. Most proofs don't give useful algorithms.
Yes.
Mathematics _can be_ formalised. But no-one writes mathematics that way. First, because when a mathematician finds he has a proof the first thing on his mind is to publish ASAP to stop anyone else getting there first and taking all the credit, second because in practice writing in formal logic (or even mainly in formal logic) leads to long, boring, unclear proofs which do not enhance reputation the way a relatively short clear proof does. A boring proof is a sequence of equations and formal logic; this sort of thing is really only used when proving a little lemma that's almost obvious anyway. Most proofs will look something like the following (LaTeX) discussing a Frechet algebra F; B_n are the Banach algebras associated to the seminorms of F, the pi_n are projections from F to B_n, the d_n are the chain maps between the B_n:
\ Delta(B _n)\]
\begin{lemma} We may naturally identify continuous homomorphisms to $\mathbb C$ from $F$ and from the $B_n$, and so write
\[\Delta(F,\mathbb C)=\bigcup_{n=1}^{\infty}\Delta(B_n,\mathbb C)\]
\end{lemma}
\begin{proof}
If $\theta:B_n\rightarrow \mathbb C$ is a continuous homomorphism then so is $\theta\circ d_n:B_{n+1}\rightarrow \mathbb C$. Since $d_n$ has dense range, different $\theta$ give different $\theta\circ d_n$ and we may identify $\theta$ with $\theta\circ d_n$. Since also $\pi_n$ has dense range, we may identify $\theta$ with $\theta\circ \pi_n$. This allows us to write
\[\Delta(F)\supseteq\bigcup_{n=1}^{\infty}
and it remains only to show that there are no extra continuous homomorphisms. \\
Suppose then that $T$ is a continuous homomorphism from $F$ to $\mathbb C$. In particular, $T$ is continuous at $0$, i.e. there is an open neighbourhood $U$ of $0$ such that $|T|1$ on $U$. This set is open in the inverse limit topology, i.e. is the intersection of the inverse limit space and an open set in the cross product of the $B_n$ with the product topology. $U$ may be assumed to be a set in a basis for the topology, so that it is the intersection of the $\pi_j^{-1}(U_j)$ for some $U_j$ open in $B_j$, up to some finite n.
Since the $d_j$ are continuous, however, this intersection must contain $\pi_n^{-1}(V)$ for $V$ an open neighbourhood of 0 in $B_n$, the intersection of the inverse images of the $U_j$. \\
We now show that $T=\theta\circ \pi_n$ for some $\theta\in\Delta(B_n)$, i.e. that $T(a)$ depends only on $a_n$, or that if $a_n=0$ then $T(a)=0$: if $a_n=0$, then $ka_n=0$ for all $k$, so $ka \in \pi_n^{-1}(V)$, and $|T(ka)|1$, for all $k$. But then $|T(a)|=0$ as required.
\end{proof}
That's a bit like saying that the obvious and most reliable way to measure the weight of an object is to atomise it, count all the atoms of each type, and add up. In other words, it works, it will give you the right answer, but it takes far too long to be of any practical use.
If you wrote out the proof of Fermat's Last Theorem in formal logic without leaving gaps, for example, you'd end up with a stack of pages several metres high.
Cunning clue here: if there is a problem which took mathematicians a century to prove true, and you think there is a trivial reason why it is false, then you are wrong. In this case, because you don't have to use all four colours with the states along the top.
A computer can prove any theorem, if you give it long enough.
Reason: a theorem is a statement which has a proof. A proof is a finite sequence of logical statements. You can order all sequences of logical statements by lexicographic order within the sum of the number of variables used and the number of statements; then simply have a computer run through all sequences of logical statements in that order, checking each one to see whether the statements in the sequence are either axioms or follow by the rules of logic from the axioms, and checking whether the final statement is the statement you want to have proved. The computer will eventually reach a proof of whatever theorem you asked it to prove. Note that if you asked it to prove a statement which is not a theorem, it will never stop. Goedel's theorem tells us that there are some statements where not only will the computer fail to prove the statement true, it will also never prove the statement false.
The problem with trying to do this in practice is that for any interesting problem the shortest proof might not fit in a telephone directory - and the computer would be trying to find it by checking through all sequences of that size. It would take far too long.
The theoretical problem you refer to is whether one can write a program which will correctly classify all statements as true or false - this is not possible; some statements are neither. If you allow it to classify as 'neither' as well, it is still not possible - the sketch above will never classify any statement as 'neither' because with such statements it never halts, for example. Turing proved that no program can correctly classify all statements.
You're thinking about chromatic number of a graph, where you colour edges of a graph.
However, when you colour regions (or countries, or however you want to look at it) then maybe this country is touching a million other countries, but I will be able to find a way of colouring all those other countries using only red, green and blue, and I will still be able to colour the whole map with only four colours.
(this has nothing really to do with real world geography maps, it just happens to be a nice way to visualise things)
It is very easy to produce a validator which correctly classifies valid and invalid proofs written in formal logic. It is very easy to prove that the validator does what it is meant to do.
We don't know whether this abstract formal logic thing actually has any resemblance to the real world - that is not Goedel's theorem, which assumes logic to be valid and discusses potentially interesting frameworks for mathematics. Whether formal logic 'works' is simply something you have to believe, you cannot argue it, for the obvious reason. Whether you can use formal logic to demonstrate that your mathematical axioms are consistent is not obvious; Goedel's theorem states that in fact whenever your mathematical axioms are strong enough to produce interesting mathematics, you cannot demonstrate consistency.
The reason why mathematicians do not like computer proofs (as much as normal proofs, anyway) and do not like computer validation (always) are:
Computer proofs tend not to give any insight into why a statement is true. They simply check vast numbers of cases, when there might exist a simple argument which gives understanding. However, there is usually interesting mathematics involved in reducing the original problem to something which can be computer checked.
It is not easy to produce a program which will verify a proof written by a normal person, in the same way that it is hard to write a program which can spot contradictions in any argument written in natural English.
An argument written out in formal logic, although easy to verify for a computer, is generally much, much longer than the same argument written by a normal person, and even if you wanted to read the telephone-directory sized proof, the interesting ideas are so dispersed that you would gain no understanding from the proof.
So, a computer verifier would only be useful when a proof is written in formal logic - which only a computer would do for a proof of any interesting statement. But the computer proof won't give a mathematician any understanding of why the statement is true, so the mathematician doesn't like it. Furthermore, because formal logic is so long-winded, it doesn't seem likely that a computer will ever be able to prove interesting statements by doing a simple bash out formal logic until it works approach. IMO, a computer program which can prove interesting mathematical statements in sensible amounts of time will be about as hard to write (and probably not too dissimilar to) a Turing-capable program.
It's technically possible, and actually quite easy, to build a detector that will tell you when a TV is operating nearby. You could build a detector that will find computers; stuff like the HDD give off a fairly unmistakable signal. But it would not be easy or cheap.
In any case, the 'detector vans' the TV licensing supposedly use are no more than a scare story. The TV licensing people simply go round and pester anyone who does not have a TV licence; they assume everyone has a TV.
This new tax idea isn't supposed to happen before 2017, by which time supposedly TV will not be RF broadcast as it is now, but transmitted over broadband lines which will also be used for Internet access etc. So chances are they will decide that what actually should be taxed is the broadband connection itself, not the PCs.
Basically, you can look at light, or electrons, or whatever, as either a particle or a wave. Sometimes one interpretation will work better (light as a particle explains the photoelectric effect, light as a wave explains interference patterns, diffraction, etc). Current state of play is that the wave interpretation is always the best way to look at things, except when you observe the system everything collapses to particles, and when something mathematically inconvenient happens (you can explain the photoelectric effect in terms of waves, but the maths is horrible).
Classic two slit experiment with light consists of shining laser light on a barrier with two slits; each slit produces a diffraction pattern (http://en.wikipedia.org/wiki/Diffraction), the diffraction patterns interfere to produce the classic two slit pattern, see same link. This basically works because the laser light is coherent, you can (sort of) treat all the photons coming from the laser like one photon.
If you do this with electrons, because electrons are waves, you get the same patterns. Ditto any other particle.
Even if you do this experiment firing only one electron at a time you will get the same two-slit interference pattern, although 'common sense' tells you the electron can only pass through one of the two slits what actually happens is it passes through both at once. If on the other hand you fit a detector over one slit to register the passage of electrons, so you can tell which slit the electron passes through, you lose the interference pattern, you get two overlapping single slit diffraction patterns, which is not the same thing.
Roughly, if you have two slits and whenever an electron is fired at the slits you do not know which slit it went through, but the classical probability (what you'd expect if you didn't know quantum mechanics) of either slit is 0.5, then you will get a two-slit pattern.
This is basically the same experiment, except instead of two slits in space a little distance apart there are two possible source times for the electron, separated by a small time gap. There is no way to know whether a detected electron was produced at the first or second time, so the maths works out (roughly) the same as for the two slits in space case and you would expect to see the classic two-slits pattern. But it is kind of neat that someone's actually found a way to test that idea.
Unless it's been settled recently, there _might_ be an infinite number of Mersenne primes, but last I heard no-one had proved that.
Why bother constructing a phony reader? Just buy one of VISA's standard ones, and stick a bit of software on it that charges $24.99 every time it can find a card in range.
Of course, the problem here is that when a thousand complaints come in to VISA HQ from people asking what the hell this charge is for, VISA take about three seconds to see that all the complaints refer to your merchant account and you get jailed. A phony reader or whatever makes no difference here - you may be able to fake out the card, but to get money you have to give VISA an account number to transfer money from and your account to transfer money to. And that is enough for VISA to catch you when complaints come in.
Offhand, the only immediately obvious way you can safely make money out of this is to make yourself a broadcast and amplify kit, which you can scan for your $20 of shopping at the supermarket, and hope that someone else (like the next guy in the queue) is near enough to you that his card activates and pays for you. Even that would be both very hard to do (magnetic induction powering a card a few feet away would be pretty hard to manage).
> What is next? Per clock cycle licensing?
That was next a few years ago. People made a huge fuss and Oracle backed down, but they did try to charge per FLOP, IIRC.
First, because scheduling everything is much easier when you only have to worry about one clock speed (or at least, only a few multiples of one clock speed).
Second, because once you've set up a production process which can fab latest and greatest processor on one half of the die, it's really not much more expensive to fab a second latest-and-greatest on the other half than a four years old core. It's not two chips, it's one chip which has two processors on it.
Slightly biased comparison, IMO.
I'd point out that in fact pattern recognition is a major component to chess play. But because the patterns are so simple, all the pattern recognition is done in the first second or so of your turn. The rest of the turn is analytic thinking. Good example of this is when you play 1 or 2 minute chess - you never have time to think about it, all your time is spent recognising patterns and responding. You can get in about 1 move a second like that, but the level of game play only drops to what you'd expect in a normal game between players ranked about 100-150 points lower.
Whereas with go (note: my play is poor) you can only get away with auto-responding to patterns when you're in a very restricted situation; trying it when you're playing in a large area will lose you the game.
If you've just spent $300 on your new P4, why would you buy a graphics card at $200 which has an order of magnitude more computing power?
Hint: general purpose CPU doing specific job => slow. Custom designed hardware for specific job => faster and cheaper.
UK law would have Lindows lose that case, anyway: it's a name designed to have a similar sound to the MS trademark and competing with said MS product. IOW, calling it 'Lindows' was a stupid idea in the first place.
Whereas MAME existed way before Ultracade, so per UK law Ultracade would lose its trademark on 'MAME' as soon as MAME objected.
To some extent, even if a savant was producing poly-time solutions, it might not indicate that they were using a better algorithm.
NP-complete essentially means a problem which is as hard as possible given you can check the solution is right in polynomial time. It follows that an infinitely parallel computer (e.g. a quantum computer) can solve all NP problems in polynomial time; if a savant were essentially acting as a massively parallel computer then your experiment might return a polynomial time solution simply because you never tested the savant with large enough problem sizes to stop them being run in parallel.
Go and read about Ramanujan.
He pretty much taught himself maths out of a exam-cramming textbook. Result being that he didn't know what a formal proof was until he came to England, and he never had any interest in repeating himself and going over the logic again. He produced proofs himself for some theorems, and left enough clues for other people (Hardy) to reconstruct his proofs for the rest of his theorems. Then there are a fair number of conjectures, some of which Ramanujan said he'd solved, most of which he didn't.
And in fact forming a useful conjecture is not easy. It's not hard to form an incredibly difficult conjecture which no-one solves for many years, it is hard to form a conjecture which you might reasonably expect to be able to solve.
By the way, FLT was called that because Fermat left behind a lot of statements which he claimed to be true. Most of them he had written solutions for, although usually not actually attached to the statement (he tended to demonstrate his cleverness by solving problems other people put up, some general proofs were found in these solutions). Some of them were proved true by other mathematicians after Fermat's death, no-one knows whether Fermat ever had a proof. A few of them were plain wrong (such as a conjectured formula which always took prime values - it didn't). But because these conjectures often were in fact true, and fairly frequently the mathematician who found a proof discovered that the same logic could be found elsewhere in Fermat's works, so that Fermat probably had in fact had a proof, there was a tendency to label all of those conjectures as theorems requiring proof. The Last Theorem was the one left over after all the others had been settled.
Yes, but there are interesting things in maths and there are less interesting things.
A table of all primes up to N is very interesting, lots of things to see.
A general theorem is usually interesting.
Spending a long time finding Mersenne primes is boring. We already know just about everything we want to know about Mersenne primes; the only major open question is whether there exist infinitely many, and that can't be answered by searching. A long string of 1s is not interesting, even when there are a prime number of 1s, and even when the binary number given by that string is itself prime. It's interesting that such things exist, and that there are nice algorithms for primality, but we already know that.
> Yes, and no single program can use an
:-)
> infinite amount of space. So, if you
> are given an arbirtary program that will
> produce an output then you can compute that
> output using only finite memory.
But you do not (in general) know how much memory will be used until after you've run the program - if you have N amount of memory and attempt to run the program then almost surely you will fail, for any given N.
I think we've got to about the same place in this argument, though