Viewing profile — kevinbuzzard

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 …

A discussion by Boris Alexeev on recent events in AI + mathematics

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 …

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 n…

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.…

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 n…

(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 …

(I'm the author: yes, it was beta tested on many Imperial College London mathematics undergraduates)

I see! So I guess the proof of the pudding will be in the eating :-) Can you do algebraic geometry?

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…

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 argum…

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 wher…

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…

Do we really know for sure that GPT4 has not seen this problem already?

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, …

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…

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 …

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 anywa…

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.

Thanks so much! Fixed.

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…

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 of…

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 pro…

Lean and the other theorem provers turn mathematical proofs into levels of a computer puzzle game, much like a chess puzzle.