Advertisements
Author Archives: xenaproject
Does anyone “know” a proof of Fermat’s Last Theorem?
So there’s a piece in Vice which quotes me as saying that I fear “all published maths is wrong”. Of course this is nonsense: indeed, as every mathematician knows, some published maths is wrong, but the vast majority of it … Continue reading
Posted in Uncategorized
Tagged Brian Conrad, Fermat's Last Theorem, Frank Calegari, Langlands-Tunnell
9 Comments
IMO 2019 Q1
Someone sent me a link to this year’s IMO questions this afternoon at work, and the first one caught my eye because it looked like a relatively straightforward functional equation question: find all such that . I’ve seen enough of … Continue reading
Lean does not (yet) have real manifolds.
Lean does not yet have real manifolds, but there has been recent progress. Continue reading
Posted in General, Imperial, undergrad maths
Tagged Agda, Bochner Integral, Coq, HOL-Light, Idris, Isabelle-HOL, Jeremy Avigad, Johan Commelin, lean, manifold, Mizar, Patrick Massot, Perfectoid Spaces, Sebastien Gouezel, theorem provers, UniMath, Zhouhang Zhou
7 Comments
A computer-generated proof that nobody understands
Computers can find 1000 page proofs about simple things. Why not Shimura varieties? Continue reading
Proofs are not programs
A proof, in the sense understood by modern mathematicians, is not always a program. Continue reading
Posted in computability
Tagged axiom of choice, bytecode, computability, Curry-Howard
Leave a comment
The inverse of a bijection.
Constructing the inverse of a bijection in Lean can be tricky for beginners. Continue reading
