Lean in practice and "sorry"

Stream: new members

[Abraham Solomon]

Hey all,

This is a bit of a meta question -- in my limited experience with math research -- i saw a common pattern is to of course cite peer reviewed work and use referenced theorems.

Naturally, unless the series of results is already written in Lean -- one choice is to backtrack and go down the citations to 'bedrock' then reprove everything in Lean until you can finally work on your result.

What is the experience of people using Lean like this? It is very tempting to simply introduce such theorems with "sorry" and work above them.

[Kevin Buzzard]

The proof of Fermat's Last Theorem uses so many other things that we're starting at the top and reducing the claim to many more technical claims which we'll worry about later