Xena
Mathematicians learning Lean by doing.
Skip to content
  • Home
  • About Xena
  • Student projects
  • What maths is in Lean?
  • Installing Lean and mathlib
  • Twitter
  • Useful links.

Category Archives: rigour

Rigorous mathematics

Posted on December 7, 2019 by xenaproject

What is rigorous mathematics? Jaffe and Quinn have some ideas, which I re-interpret a little. Continue reading →

Posted in rigour, Uncategorized | Tagged Bill Thurston, Brian Conrad, Coq, David Hansen, Dominic Verity, Dustin Clausen, Emily Riehl, Frank Calegari, George Boxer, Isabelle-HOL, Jaffe and Quinn, Johan de Jong, metamath, Mizar, Mochizuki, Peter Scholze, rigour, Toby Gee, UniMath, Vincent Pilloni, ZFC | 10 Comments
  • Categories

    • Algebraic Geometry
    • computability
    • General
    • Imperial
    • Learning Lean
    • M1F
    • M40001
    • M4P33
    • number theory
    • Olympiad stuff
    • rigour
    • tactics
    • Technical assistance
    • Type theory
    • Uncategorized
    • undergrad maths
  • Recent Posts

    • Lean Together 2021 January 12, 2021
    • The end of the summer. January 9, 2021
    • Liquid tensor experiment December 5, 2020
    • Thoughts on the Pythagorean theorem September 19, 2020
    • Two types of universe for two types of mathematician July 23, 2020
Xena
Blog at WordPress.com.
Privacy & Cookies: This site uses cookies. By continuing to use this website, you agree to their use.
To find out more, including how to control cookies, see here: Cookie Policy