Proof network and knowledge repository
mars 16th, 2008
I have been looking a long time for a way to represent on the web a mathematical corpus. It would be tremendous if one could find on the web the different books written on a subject, in a form that enables verification of theorem and proof.
Let’s reflect on what a lesson is. Mostly a lesson is about learning one by one different entities, and the relations that those entities share. It is all about serializing a graph.
If we were to improve this process of learning, we should identify what represent the most effort and the least added value in the making of it, and I see 3 big bottleneck.
- This process has to occur at a level the audience can understand. The same lesson can take a day or 5 minutes depending on the knowledge of the audience. One of the big problem that clutters reuse of lessons on a large scale basins is that every time one wants to adapt the level, a whole rewrite is necessary.
Having a formal representation of books would allow for seamless rewrite of proof down to the basic axiom if necessary.
- Another variability is how does one reuse the theorem or presentation of another. Dissemination now is informal, slow, and based on individual reading. Few ways exists to have clever solution to emerge. A repository of steps for proofs, which would allow reuse in other context, would enable indirect voting, and promote the best practices.
- Finally, another problem is the sheer size of the domain which can only be tackled with by many specialists. Sometimes the difficulty lies not in the domain itself but in the many ways there are to show one same effect. There is no place for such collaboration to take place in a fruitful way, with people ranging from high school students to phd’s to contribute and enrich each other. Sure, wikipedia exists, but is completely out of scope : what if I was to see the 10 differents ways to prove an assertion, and how the theorems used apply in the specific case i am looking at ? wikipedia can’t handle this kind of data explosion and no onewill contribute this to the details I might need (and some other person won’t)
So, facing those issues, one might think that the computer science people in universites found a way ? No, you want to know why ? They are research ways not tho share proof and have a formal system for proof and representation. no. they are waaaaayy behond that : they are looking to automate the creation of proof.
This really is for me the completely wrong way to go, and we should first concentrate on having a formal description system to tackle those 3 points I exposed. Then, with such a useful formal description, will we get ammo for automated proof, if we ever can solve it.
Fuse
septembre 22nd, 2007
Getting a list of your activerecord models
septembre 13th, 2007
Ripping off investors
août 25th, 2007
Really cheap programming
juin 17th, 2007
Big corporations can get a really good deal, with PPI. featuring programmers as cheap as 60 cents/hour. With such a price, you can get a hundreds of them for cheap labor and have them work on your business critical missions.
“Humans and higher primates share approximately 97% of their DNA in common. Recent research in primate programming suggests computing is a task that most higher primates can easily perform. Visual Basic 6.0™ was the preferred IDE for the majority of experiment primate subjects.” Read More about the research of Dr. James McAuliffe.
Do not miss Primate programming Inc.
Topic map inference at google
juin 17th, 2007
Blog et dépendances
juin 9th, 2007
- Very specialized on a technical subject
- At a forking point on a topical and applicative subject
- my technical geeky posts about Linux, MacOs, and other system-oriented issues on Technofinance
- my math and theoretical posts on xQuant, which intends to be more of an applicative forking point
xQuant extends its empire
juin 3rd, 2007
In a brilliant demonstration of technical expertise and non-conformist brio, that is, of utter elegance, xQuant is now equipped with a Wiki section that will enable users to render their thoughts in plain English and Latex.
This Wiki is particularly meant to be used to develop themes including inference, categories, and stochastic finance.
A probability problem and some Ruby
mai 12th, 2007
Do the player's chances of getting the car increase by switching to Door 2?
The answer is yes. There are different ways of looking at the pb. One is to go on with computation after having a clear view of what to compute. In situations like this, you need to deal with the information given to you, namely the door opened for you. Then one has to always pick the door with the highest probability conditioned to all the information given. In this case, we just know the result of some operation the host did. This is typically where to use the Bayes theorem, as it enables us to revert the conditioning to a probability we know, since we know the process followed to pick the opened door. So if we compute the probability of each possibility we have : c1, c2, c3 denote that the corresponding door has a car behind o2 denotes the fact that the door 2 has been opened p1 denotes the fact that you picked the door 1 in the first place- P (c1 | o2, p1) = P ( o2 | c1, p1) * P(c1 | p1 ) / P(o2 | p1 ) = 1/2 * 1/3 / 1/2 = 1/3
- P (c2 | o2, p1) = P ( o2 | c2, p1) * P(c2 | p1 ) / P(o2 | p1 ) = 0 * 1/3 / 1/2 = 0
- P (c3 | o2, p1) = P ( o2 | c3, p1) * P(c3 | p1 ) / P(o2 | p1 ) = 1 * 1/3 / 1/2 = 2/3
- P ( o2 | c1, p1) = 1/2 because if p1 happens, the host will have to pick between door 2 and door 3 to open, and since the car is behind door 1, he has no other constraints. chance are therefore 1/2 he'll pick up door 2.
- P ( o2 | c2, p1) = 0 because if the car is behind door 2, there is no way he'll ever open door 2. Also, P ( c2 | o2 ) = 0 so that P (c2 | o2, p1) = 0 too so we don't even have to compute this.
- P ( o3 | c2, p1) = 1 because if p1 happens, the host will have to pick between door 2 and door 3, but the car being behind door 2, he'll have no choice but to pick the door 3
puts('===Monty Hall, classic version===')
ProbabilityTree.runreport(1.to_r) { |u|
treasuredoor = u.choose(1,2,3)
guessdoor = u.choose(1,2,3)
remaining_doors = [1,2,3].select{ |x|
x != treasuredoor and x != guessdoor }
showdoor = u.choose(*remaining_doors)
if (treasuredoor == guessdoor)
u.report "You should stay"
else
u.report "You should switch"
end
}.display
Produces: ===Monty Hall, classic version=== You should switch ==> 2/3 You should stay ==> 1/3This piece of code illustrates the flexibility of lambda function, as it enables to completely dissociate a particuliar drawing (you win, you loose) to the context in which it is used ( here, it is used to draw up a certain number of simulations, and accumulate the results to see which is more likely)