Skip to main content
MathOverflow

Return to Answer

Changed link to point to the formalisation, not Holmes' own website (probably was a typo)
Source Link
David Roberts ♦
David Roberts ♦
  • 35.5k
  • 11
  • 124
  • 349

It has indeed been exhausting. I can report that the situation seems to have been resolved. The central hard part of the latest version of my Con(NF) proof has been verified in Leanhas been verified in Lean by Sky Wilshaw, a Part III student at Cambridge. There remains the substantial project of cleaning up the paper (which has been improved by two years of dialogue with the verifier) and tidying up the formalization and making all available. But I can report firmly that the result is correct.

It has indeed been exhausting. I can report that the situation seems to have been resolved. The central hard part of the latest version of my Con(NF) proof has been verified in Lean by Sky Wilshaw, a Part III student at Cambridge. There remains the substantial project of cleaning up the paper (which has been improved by two years of dialogue with the verifier) and tidying up the formalization and making all available. But I can report firmly that the result is correct.

It has indeed been exhausting. I can report that the situation seems to have been resolved. The central hard part of the latest version of my Con(NF) proof has been verified in Lean by Sky Wilshaw, a Part III student at Cambridge. There remains the substantial project of cleaning up the paper (which has been improved by two years of dialogue with the verifier) and tidying up the formalization and making all available. But I can report firmly that the result is correct.

Added link to webpage
Source Link
Timothy Chow
Timothy Chow
  • 82.7k
  • 26
  • 363
  • 587

It has indeed been exhausting. I can report that the situation seems to have been resolved. The central hard part of the latest version of my Con(NF) proof has been verified in Leanhas been verified in Lean by Sky Wilshaw, a Part III student at Cambridge. There remains the substantial project of cleaning up the paper (which has been improved by two years of dialogue with the verifier) and tidying up the formalization and making all available. But I can report firmly that the result is correct.

It has indeed been exhausting. I can report that the situation seems to have been resolved. The central hard part of the latest version of my Con(NF) proof has been verified in Lean by Sky Wilshaw, a Part III student at Cambridge. There remains the substantial project of cleaning up the paper (which has been improved by two years of dialogue with the verifier) and tidying up the formalization and making all available. But I can report firmly that the result is correct.

It has indeed been exhausting. I can report that the situation seems to have been resolved. The central hard part of the latest version of my Con(NF) proof has been verified in Lean by Sky Wilshaw, a Part III student at Cambridge. There remains the substantial project of cleaning up the paper (which has been improved by two years of dialogue with the verifier) and tidying up the formalization and making all available. But I can report firmly that the result is correct.

Source Link
Randall Holmes
Randall Holmes
  • 571
  • 2
  • 5

It has indeed been exhausting. I can report that the situation seems to have been resolved. The central hard part of the latest version of my Con(NF) proof has been verified in Lean by Sky Wilshaw, a Part III student at Cambridge. There remains the substantial project of cleaning up the paper (which has been improved by two years of dialogue with the verifier) and tidying up the formalization and making all available. But I can report firmly that the result is correct.