My hobby: proof engineering | Stephan Boyer

december 2018 by mcherm

An article from someone who's hobby is doing mathematical proofs in coq. Excellent footnotes.

coq
math
proof
via:reddit
december 2018 by mcherm

Two-hundred-terabyte maths proof is largest ever : Nature News & Comment

may 2016 by mcherm

Proof by exhaustive examination of cases.

math
proof
via:HackerNews
may 2016 by mcherm

Is there a rigorous way to say when two proofs of the same theorem are similar? : math

june 2015 by mcherm

Some thoughts on comparing proofs: when are two proofs equivalent?

math
via:reddit
philosophyOfMath
logic
proof
june 2015 by mcherm

A Computer Scientist Tells Mathematicians How To Write Proofs | Roots of Unity, Scientific American Blog Network

january 2015 by mcherm

A proposed better way to write proofs. I need to check it out; this could be big.

math
proof
via:HackerNews
january 2015 by mcherm

Voevodsky’s Mathematical Revolution | Guest Blog, Scientific American Blog Network

december 2013 by mcherm

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

january 2012 by mcherm

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

june 2011 by mcherm

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

august 2010 by mcherm

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

august 2010 by mcherm

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

april 2010 by mcherm

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

march 2010 by mcherm

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

november 2009 by mcherm

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.

math
proof
haskell
philosophy
november 2009 by mcherm

The Universe of Discourse : A new proof that the square root of 2 is irrational

october 2009 by mcherm

A simple, elegant geometric proof that sqrt(2) is irrational.

math
proof
via:reddit
october 2009 by mcherm

The L4.verified project A Formally Correct Operating System Kernel

august 2009 by mcherm

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

Astrologers fail to predict proof they are wrong

april 2008 by mcherm

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

march 2008 by mcherm

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

february 2008 by mcherm

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: