lean_workbook_plus_50827

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

We can see that $2^{1398}+1=6917257425689530036622985546718721032458048899171898480735288332161153759265304724368239531227090326307349383041499823466971386343244651801294157545363169233480268460307612535996044740389512799159954588308125393833558110056091314603315306137267161874183473373214673459734004841723514031219907235701547001390855970990191853377446857678811103668220504652391954935598744989572362036837653935170399380502807145490246317113345$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50827 : (2^1398 + 1 : ℤ) = 6917257425689530036622985546718721032458048899171898480735288332161153759265304724368239531227090326307349383041499823466971386343244651801294157545363169233480268460307612535996044740389512799159954588308125393833558110056091314603315306137267161874183473373214673459734004841723514031219907235701547001390855970990191853377446857678811103668220504652391954935598744989572362036837653935170399380502807145490246317113345   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph