kevinbuzzard

7 ms·

31.
by kevinbuzzard 6y ago
This is a milestone result, and its formalisation taught us many things, for example that the systems are capable of handling long proofs about elementary objects. However finite graph theory is not remotely mainstream mathematics. Take y
32.
by kevinbuzzard 6y ago
The problem with metamath is that you basically have to be a fully signed-up masochist in order to do anything nontrivial with it. People have certainly done nontrivial things with it e.g Carneiro and the prime number theorem -- but it take
33.
by kevinbuzzard 6y ago
Hi! Yes! Just pick a different one! The problem is that constructivists have been formalising mathematics for decades and have not really managed to break through into the mainstream mathematical community with their efforts. The difference
34.
by kevinbuzzard 6y ago
Yes, this is very old. This is a review of Lean 3; Lean 4 is about to appear and this deals with several of the issues flagged by Hales, for example speed.
35.
by kevinbuzzard 6y ago
blah blah blah type checkers blah blah blah can be run on different chipsets / OS's blah blah blah computers are several orders of magnitude more accurate blah blah blah not really the issue.
36.
by kevinbuzzard 6y ago
[just to be clear here, I am the author of the Xena project blog and my current research is in formalising number theory; before formalisation I was working in Scholze's area.] Scholze's first application of the theory of perfecto
37.
by kevinbuzzard 6y ago
I seem to be associated with that quote (and of course I didn't say it -- indeed when I spoke to Quanta I used factorials plus one). When the article appeared I emailed Kevin Hartnett immediately to suggest replacing that line with som
38.
by kevinbuzzard 6y ago
(disclaimer: I'm the author of the blog post). The argument the other way is that if a mathematician sees this convention, their reaction is likely to be "that's just silly, 1/0 is obviously 'halt and catch fire&#x2
39.
Sphere Eversion: A Formal Blueprint(leanprover-community.github.io)
2 points by kevinbuzzard 6y ago|0 comments
40.
by kevinbuzzard 7y ago
I totally agree that it's all over the place. I am a mathematician and have just thrown this together because I wanted my students to be able to learn Peano arithmetic (something I teach in my course) in a fun way. I am in desperate ne
41.
by kevinbuzzard 7y ago
I used Patrick Massot's Lean Formatter https://github.com/leanprover-community/format_lean to make the Lean web page with the analysis theorem on, and Mohammad Pedramfar's Lean game maker was very much inspir
42.
by kevinbuzzard 7y ago
First let me point out that you can jump to any level at any time, so you lose your progress, but only in a weak sense, if you lose your browser tab. You do lose your proofs though. The natural number game was made by passing a repository w
43.
by kevinbuzzard 7y ago
Automation of epsilon-delta proofs is in its infancy. Currently with an interactive theorem prover like Lean, you type in the proof yourself, so it's pretty much exactly the same as doing it on paper, except that you can't make
44.
by kevinbuzzard 7y ago
Lean's maths library development is essentially completely focussed on classical mathematics, which is why it has been so successful in drawing "working mathematicians" in. Such people do not care at all about the issues invo
45.
by kevinbuzzard 7y ago
There is a huge amount of evidence of mathematics undergraduates using interactive provers, which they weren't doing before. There are very few profs using any interactive prover, because currently these things offer nothing useful to
46.
by kevinbuzzard 7y ago
Contains a section on the rational and real numbers. Mathematicians might want to start at section 11.5.
47.
by kevinbuzzard 7y ago
[Here]( https://arxiv.org/abs/1907.01449 ) is a Lean formalisation of a 2017 Annals of Mathematics paper.
48.
Lean Book: The Hitchhiker's Guide to Logical Verification [pdf](github.com)
177 points by kevinbuzzard 7y ago|19 comments
49.
by kevinbuzzard 7y ago
I was being intentionally provocative. On the other hand I feel like there are plenty of people in my (mathematics) department who would say that "normal" fields like geometry, topology, algebra, number theory and analysis are whe