feat(Other/Rule30): Wolfram's Rule 30 Prize Problems (non-periodicity & equal frequency)#4377
feat(Other/Rule30): Wolfram's Rule 30 Prize Problems (non-periodicity & equal frequency)#4377Deicyde wants to merge 1 commit into
Conversation
|
👋 This is an automated welcome message. 🤖 A few friendly reminders while the review gets started:
Thanks again for helping improve Formal Conjectures. |
|
Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA). View this failed invocation of the CLA check for more information. For the most up to date status, view the checks section at the bottom of the pull request. |
|
@googlebot I signed it! |
Thanks! But Claude didn't, so it needs fixing: one way to do this is to amend the commits and remove Claude as co-author and then force push... |
…city & equal frequency) Formalize Problems 1 (center column not eventually periodic) and 2 (running average of the center column tends to 1/2) from Wolfram's 2019 Rule 30 Prizes, as sorried open-problem statements in the answer(sorry) ↔ P idiom. Placed in Other/ (sourced from Wolfram's announcement + rule30prize.org, not a Wikipedia article). The Rule 30 encoding is checked against OEIS A051023 via a @[category test] lemma. Problem 3 is omitted: it is an all-algorithms computational lower bound with no canonical model-independent phrasing.
Deicyde
force-pushed
the
add-rule30-prize-problems
branch
from
2d7ac10 to
4b19f67
Compare
|
@mo271 Fixed, thanks |
2 participants
Summary
Adds a Lean formalization of two of Stephen Wolfram's three Rule 30 Prize Problems (2019).
Changes
FormalConjectures/Other/Rule30.leanDetails
Defines Rule 30 (
c' = l ⊕ (c ∨ r)) and its center columncenterColumn : ℕ → Bool, then states two of the three prize problems:centerColumn_not_eventually_periodic— Problem 1: the center column is not eventually periodic.centerColumn_frequency_half— Problem 2: the running average of its values tends to1 / 2.References included: