2

I just discovered Lean and using computers for stating and proving theorems. The first question that came to my mind, can we write any proof with Lean? Or are there limitations (something that you can write a proof for on paper but not in Lean)?

I'm not talking about practicality or feasibility. But does the Lean system have the capability?

Edit: I posted the same question on proofassistants.stackexchange.

Hatchi Roku
  • 187
  • 7
  • Do you limit the scope of the question to things mathematicians would prove in a standard logical/foundational framework that could be used under 90% of today's mathematics? Or do you want to account for fringe approaches/work on foundations, too? – Mark S. Aug 15 '23 at 11:17
  • 1
    FYI, I believe questions like yours, about proof assistants like Lean, may be better asked instead on the relative new SE site Proof Assistants, which has a description of "Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants". Note a site search for the "lean" tag currently shows $108$ questions. However, before possibly posting there, search look for any possible duplicates, check their ... – John Omielan Aug 15 '23 at 12:27
  • (cont.) help center for the type of questions to ask (and not to ask), look at a least few questions in any tag(s) you might use (e.g., the "lean" one I mentioned) to get an idea of how their questions are structured, etc. – John Omielan Aug 15 '23 at 12:30
  • @MarkS. It would be nice to get an answer for both cases. But I originally meant proving in a standard framework, not the work on foundations. – Hatchi Roku Aug 15 '23 at 12:45
  • 1
    @JohnOmielan Thanks for mentioning Proof Assistant! I looked at all questions with the tag "lean". None of them was about this. I will post my question there as well. – Hatchi Roku Aug 15 '23 at 12:47
  • I got multiple good answers on the Proof Assistants thread. – Hatchi Roku Aug 15 '23 at 21:23

0 Answers0