### Abstract

This article provides a brief formalisation of the two equations known as the Sophomore's Dream, first discovered by Johann Bernoulli in 1697:

\[\int_0^1 x^{-x}\,\text{d}x = \sum_{n=1}^\infty n^{-n} \quad\text{and}\quad \int_0^1 x^x\,\text{d}x = -\sum_{n=1}^\infty (-n)^{-n}\]

### License

BSD License

### Topics

- Mathematics/Analysis

### Session Sophomores_Dream

- Sophomores_Dream

## Cite

×

Sophomores_Dream-AFP

    @article{Sophomores_Dream-AFP,
      author  = {Manuel Eberl},
      title   = {The Sophomore's Dream},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Sophomores_Dream.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- May 9, 2022 : Isabelle2021-1