kevinbuzzard

6 ms·

1.
by kevinbuzzard 2mo ago
Indeed I was being slightly tongue-in-cheek -- but if you ask geometers whether they believe the Hodge conjecture then you certainly don't always get an unqualified "yes"! This is in contrast to e.g. asking number theorists w
2.
Formalization of Erdős Problems(xenaproject.wordpress.com)
7 points by kevinbuzzard 10mo ago|1 comments
3.
by kevinbuzzard 10mo ago
A discussion by Boris Alexeev on recent events in AI + mathematics
4.
by kevinbuzzard 1y ago
That is correct, the title is currently misleading (arguably the title of every paper I ever wrote was misleading before I finished the work, I guess, and the work linked to above is unfinished). If you are interested in seeing more details
5.
by kevinbuzzard 1y ago
Right now I would say that tools like Lean are not useful for learning advanced mathematics, currently you're mostly better off with pencil and paper. This might change but right now the infrastructure/tools aren't there to m
6.
by kevinbuzzard 1y ago
Most mathematicians aren't doing formalization themselves, but my impression is that a lot of them are watching with interest. I get asked "is my job secure?" quite a lot nowadays. Answer is "currently yes".
7.
by kevinbuzzard 1y ago
Indeed. I'm not formalising FLT because I think it might be wrong -- I'm formalising it because I know the proof is correct, and using the project as an excuse to get some modern number theory into Lean's mathematics library.
8.
by kevinbuzzard 2y ago
(I'm the author of the game) Unfortunately it did not. That comment was made when I was optimistic that an undergraduate who'd added more levels as a summer project would go on to PR them, but then the term started and they were d
9.
by kevinbuzzard 2y ago
(I'm the author: yes, it was beta tested on many Imperial College London mathematics undergraduates)
10.
by kevinbuzzard 2y ago
I see! So I guess the proof of the pudding will be in the eating :-) Can you do algebraic geometry?
11.
by kevinbuzzard 2y ago
Right now, machines proving stuff which is interesting to lots of human mathematicians but unprovable by them is science fiction. People seem to have very different opinions on the following two questions: 1) Whether it will still be scienc
12.
by kevinbuzzard 2y ago
I highly doubt that the proof will get small enough to fit into a margin, but history shows that it's not at all unreasonable to expect simplifications/generalisations of the argument to come out of a formalisation (for example th
13.
by kevinbuzzard 2y ago
Lean is free and open source and nothing to do with MS. Check out https://lean-lang.org/ and https://github.com/leanprover/lean4 -- no mention of MS or MSR (where de Moura was where he developed Lean 3
14.
by kevinbuzzard 2y ago
My impression is that some parts of maths work best using set theory, some parts work best using type theory, some work best using a category-theoretic foundation and ignoring size issues etc etc. There's no one "best" founda
15.
by kevinbuzzard 3y ago
Do we really know for sure that GPT4 has not seen this problem already?
16.
by kevinbuzzard 3y ago
Here's a Lean 3 development of a bunch of topos theory https://github.com/b-mehta/topos/tree/master/src , but it's not in the maths library (and now needs to be updated to Lean 4, although the
17.
by kevinbuzzard 4y ago
Yes. Coq has been around for decades and was adopted by the software verification community. Lean is much younger and its mathematics library caught on with the mathematician crowd, meaning that much of the Lean documentation right now is f
18.
by kevinbuzzard 4y ago
Just to add my usual disclaimer: the mathlib project is a big open source project and I'm not its leader or even a maintainer of the code base. I am a contributor (as are hundreds of other people) and I talk about it a lot because I th
19.
by kevinbuzzard 4y ago
I just confirmed with Azerbayev that the typo in the example from Munkres ("identify" not "identity") was indeed what was fed to the algorithm (and the algorithm got it right anyway). We found some other funny examples w
20.
by kevinbuzzard 5y ago
PS I cannot believe my undergraduate teaching material is on HN! I am a math lecturer and this is just my course notes for my UGs.
21.
by kevinbuzzard 5y ago
Thanks so much! Fixed.
22.
by kevinbuzzard 5y ago
The fact remains though that Lean 3 worked well enough to do Scholze level mathematics. I never quite know what to make of people saying "if the designers had done it in some other way, it would have been better". Of course if som
23.
by kevinbuzzard 5y ago
Defeq undecidability is a feature of Lean in the sense that it is a conscious design decision. As we have seen both in this thread and in other places, this design decision puts off some people interested in the foundations of type theory f
24.
by kevinbuzzard 5y ago
I'm not quite sure what you're asking about. I'm saying that we can't yet take the Wiles and Taylor-Wiles proof of Fermat's Last Theorem, feed it into a machine, and get a Lean proof of Fermat's Last Theorem.
25.
by kevinbuzzard 5y ago
Lean and the other theorem provers turn mathematical proofs into levels of a computer puzzle game, much like a chess puzzle.
26.
by kevinbuzzard 5y ago
Presumably the asterix denotes "actually true"? ;-)
27.
by kevinbuzzard 5y ago
I agree, but I think my statement is accurate today in 2021. I would love to see funds directed towards this sort of question. The big problem is that at high level so so much is skipped over, and you still sometimes have to struggle to p
28.
by kevinbuzzard 5y ago
Basically it turned out that theoretical undecidability did not matter in practice, because Scholze mathematics relies so little on definitional equality. We prove theorems with `simp` not `refl`. Pierre-Marie Pédrot is quoted above as sayi
29.
by kevinbuzzard 6y ago
It's mathematics where certain kinds of proof by contradiction are not allowed -- if you want to prove that something exists because you want to use it, then you have to make it, you can't just say "let's assume it didn&
30.
by kevinbuzzard 6y ago
:-) Yes, by assuming classical logic the Lean community is taking a non-classical approach to bringing formalisation to the masses :-)

More ›