mcherm : proof   19

My hobby: proof engineering | Stephan Boyer
An article from someone who's hobby is doing mathematical proofs in coq. Excellent footnotes.
coq  math  proof  via:reddit
december 2018 by mcherm
Voevodsky’s Mathematical Revolution | Guest Blog, Scientific American Blog Network
A fields medalist says he's connected a few fielkds in math and thereby made computer proofs easier. He predicts large numbers of mathematicians collaborating using automated proof systems.
math  computerscience  proof  via:HackerNews
december 2013 by mcherm
When is proof by contradiction necessary? « Gowers's Weblog
If you examine it closely there is no clear distinction between proofs that use contradiction and those that don't. The only real metric is readability.
math  proof  logic  via:reddit
january 2012 by mcherm
An analytic approach to the Collatz 3n + 1 Problem
A proposed proof of the Collatz conjecture that applying 3n+1 to odd numbers and n/2 to even ones will terminate with 4,2,1 (repeat) for all starting values.
math  proof  via:HackerNews
june 2011 by mcherm
Shtetl-Optimized: Eight Signs A Claimed P is not NP Proof Is Wrong
The evidence that Scott Aaronson used to quickly evaluate a proposed proof of P!=NP and very rapidly reach enough confidence to bet his house on it.
ScottAaronson  computerscience  math  complexity  proof  philosophy
august 2010 by mcherm
Putting my money where my mouth isn’t » Shtetl-Optimized
Now that's one way of making your point. Scott Aaronson (a well-known blogger in complexity theory) wants to show how sure he is that the newly revealed proof that P!=NP will have flaws. But he doesn't have time to find the flaws. So he literally bets his house on it.
ScottAaronson  math  skepticism  computerscience  complexity  proof  philosophy
august 2010 by mcherm
Blogging, Tic Tac Toe and the Future of Math at Steven Landsburg | The Big Questions: Tackling the Problems of Philosophy with Ideas from Mathematics, Economics, and Physics
A leading mathematician posted to his blog that he thought a particular problem could be solved and he invited collaboration. Over about a year a huge collaboration of many people managed to push it forward until they finally succeeded in proving it. Wow. Groundbreaking!
math  philosophy  blogging  proof  collaboration  via:reddit
april 2010 by mcherm
Microsoft open-sources clever U-Prove identity framework
About a very interesting library that allows one to verify certain key information to a website (like that you're charging something to a credit card) without revealing the underlying data (like your name, address, and credit card). Also discusses why companies won't use this: it's to their benefit to collect customer data.
privacy  cryptography  microsoft  opensource  identity  identitytheft  proof  ArsTechnica  via:ArsTechnica
march 2010 by mcherm
Catching a Mathematical Error Using Haskell’s Type System « Sententia cdsmithus
The rather important math proof had an error that went undetected for 25 years until someone tried building a program for messing with the stuff, at which point it caught it. I think the most interesting lesson to be drawn is one about the definition of proof.
november 2009 by mcherm
The L4.verified project A Formally Correct Operating System Kernel
Someone has managed to produce a formal proof of the behavior of a production-quality core OS kernel. They related the C code to a Haskell program, then managed to run an automated prover on that. It's an impressive achievement!
programming  computerscience  proof  via:slashdot
august 2009 by mcherm
Euclid's Proof of the Infinitude of Primes (c. 300 BC)
An analysis of Euclid's most elegant proof. It is interesting to look at how our modern mathematical language is far better at expressing this sort of proof than Euclid's was.
math  proof  euclid
july 2008 by mcherm
Astrologers fail to predict proof they are wrong
Scientific evidence that astrology is bunk. Do we really NEED scientific proof of this?
skepticism  proof  science  astrology  via:digg
april 2008 by mcherm
the physics arXiv blog » Blog Archive » Rubik’s cube proof cut to 25 moves
New proof that Rubik's cube can always be solved in 25 or fewer moves. (It's known to take at least 20 for some configurations.) Interesting (but fairly standard) use of computer proof techniques.
math  proof  games
march 2008 by mcherm
PHYS771 Lecture 12: Proof
A math lecture about some odd corners of proofs: probabilistic proofs, zero-knowledge proofs, and arcana like that.
math  proof
february 2008 by mcherm

Copy this bookmark: