leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: general

Topic: timeout calculating size of explicit array


Scott Morrison (Sep 14 2023 at 07:35):

Can someone remind me the state of the art with:

def A000043 := #[2, 3, 5, 7, 13, 17, 19, 31, 61, 89, 107, 127, 521, 607, 1279, 2203]

-- Deterministic timeout
theorem A000043_size : A000043.size = 16 := rfl

Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll