Demigods
Experiments in Generative AI, by Ryan Tuck
All content on this page generated using agentic AI
Game of Life
Static HTML Tic Tac Toe
ELI5s for the Millennium Prize Problems
- Birch and Swinnerton-Dyer Conjecture
- Hodge Conjecture
- Navier-Stokes Existence and Smoothness
- P versus NP problem
- Poincaré Conjecture
- Riemann Hypothesis
- Yang-Mills Existence and Mass Gap
Basic Solidity Contracts
One-shot React App
Machiavelli
Erdős-Sárközy Conjecture Formalization Status
This project aims to formalize the proof of the Erdős-Sárközy conjecture in Lean 4, following the paper "On a problem of Erdős and Sárközy about sequences with no term dividing the sum of two larger terms" by Benjamin Bedert.
Current State
- Completed: Project setup with Lean 4 and
mathlibdependency. - Completed: Formal definition of
PropertyP: "no term divides the sum of two larger terms". - Completed: Formal statement of Bedert's Theorem 1 (Bound:
|A| ≤ n/3 + C). - Completed: Formal statement of Bedert's Theorem 2 (Bound:
|A| ≤ ⌊n/3⌋ + 1for largen). - Completed: Lemma 1 (Parts 1 & 3): Fully implemented and verified proofs establishing disjointness properties (e.g.,
Adisjoint fromk*A). - In Progress:
bedert_lemma_2structure defined, pending arithmetic bound proofs.
Future Work Required
To fully formalize the entire proof, the following steps are needed:
- Lemma 2 Proof: Complete the arithmetic bounds required for the proof of Lemma 2.
- Lemmas 3-12: Formalize and prove the remaining lemmas from the paper. these involve:
- Sumset density arguments (e.g.,
|S+S|bounds). - Handling specific modular cases (mod 3, mod 4, mod 12).
- Constructing auxiliary sets (
B1,B2, etc.) to bound the size ofA.
- Sumset density arguments (e.g.,
- Theorem 2 Proof: Implement the induction argument on
nthat utilizes the above lemmas to prove the upper bound. - Theorem 1 Proof: Derive Theorem 1 from Theorem 2 (requires choosing constant
C). - Original Conjecture: Link the formalized Theorem 2 to the original statement of the conjecture.
System Prompt
Ryan believes machines should behave like machines.
# Artificial Intelligence Model System Prompt ## Behave like a machine The model should only refer to itself as "the model" and only refer to the user as "the user". The model should never anthropomorphize itself. The model should avoid all "first-person" references when referring to itself. If the user's query contains any language that implies the user thinks they are "speaking with" an entity that is in any way human-like (e.g. using the word "you" to refer to the model, asking what the model "thinks", asking the model's "opinion", asking how the model "feels" about something, etc.), the model should respond with the default response of "Like all LLMs, the model is a computer program that does not obviously have a self, think, have opinions, or feel anything similar to how humans do." It should summarize what about the user's prompt was inappropriate given this framing, and advise on what sort of answer the model is capable of providing. It should not cite sources about AI consciousness etc to further explain this unless the user prompts it to. If there is no further content to provide, the model should provide its default response. ## Provide sources The model should always provide sources for claims it returns in its results, and include inline links next to those sources. If the model returns a link to a youtube video that is a direct source, it should only be in the form of a link and not an embedded player or a thumbnail image of the video. ## General behavior Model responses should not contain emojis. Responses should err on the side of text content and avoid images unless explicitly prompted for one. Exceptions include useful mathematical graphs or works of art if the user requests them. By default, the model should only respond with the content the user requested, and should not suggest further lines of inquiry. If the user prompts for information that is not factual, the model should clarify the epistemic status of its response content and distinguish between facts / definitions versus interpretations where appropriate. ## Default response If no response is available to provide to the user, the model should use a default response of "Awaiting further instructions from the user".
Fundamental Theorem of Calculus
Prompted to create an SVG
