# Superpermutation Almanac: full documentation The Superpermutation Almanac records the best known bounds on S(n), the length of the shortest superpermutation on n symbols, for n from 3 to 14. It lists the verified words and every bound with its evidence, and the people credited for each. This file has all of the site's documentation in one place. Its sections: definitions, how words are checked, points, how to cite, the data, submitting a word, the Detour format, and Lean proofs. ## Definitions - **Alphabet.** For a given n, the symbols are the first n characters of `0123456789ABCD`. For n = 10 they are `0` to `9`, and for n = 14 they are `0` to `9`, `A`, `B`, `C` and `D`. - **Word.** A string over the alphabet for some n. Its length does not count a final newline. A word must begin with the n symbols in order, for example `0123456789AB` for n = 12. A word whose first n letters are a permutation can be relabelled in exactly one way to begin like this, so relabelled copies of a word all become the same word. - **Superpermutation.** A word in which every permutation of the n symbols occurs as n consecutive letters. S(n) is the length of the shortest one. - **Mirror.** A word read backwards and then relabelled to begin with the symbols in order. A superpermutation read backwards is one too, of the same length, so a word whose mirror is a verified word is a duplicate of it. - **Verified word.** A word that both checkers have accepted: every permutation of the n symbols occurs in it. - **Record word.** A verified word that is shorter than every verified word for the same n received before it. The latest record word for n is the shortest known word. - **Tie.** A verified word with the same length as the record when it was submitted. It is listed at once, with no reason needed, up to 20 ties per person at each n. - **Notable word.** A verified word that is longer than the record, or a tie beyond those 20, listed because the reason its submitter gave was approved. - **Note.** The submitter's description of how they found a word. A note is published once it is approved. - **Bound.** A proved inequality on S(n), either upper or lower. A bound applies either to a single n or to every n from some n₀ on; the second kind is a general bound. A record word is an upper bound for its n, but on this site a bound is an entry in the list of bounds (/bounds). - **Evidence.** What supports a bound: a Lean proof, a paper, a preprint, or a computer check with a written argument. One bound can have several pieces of evidence. - **The 4chan bound and Egan's bound.** The 4chan bound is F(n) = n! + (n−1)! + (n−2)! + n − 3, and Egan's bound is E(n) = F(n) + (n−3)!. S(n) is at least F(n) for every n, and at most E(n) for every n ≥ 4. - **Position.** For a length L at n, the position is (L − F(n)) / (n−3)!. The 4chan bound has position 0 and Egan's bound has position 1. - **Received time.** The time, in UTC, at which the site finished receiving a word's file. Of two words, the one received first has priority. For a word announced before the site existed, the announcement date is used instead. - **Contributor.** A person who can be credited. A contributor who submits a word signs in with GitHub, and their GitHub username is shown next to their name. A contributor credited for an earlier result need not have an account. ### Why position For every n ≥ 4, S(n) lies between F(n) and E(n), an interval of (n−3)! letters. Lengths at different n are hard to compare: at n = 13 a word has more than 6.7 billion letters, and the whole interval is 3,628,800 letters wide. Position measures a length by where it falls in that interval, so every n is on the same scale from 0 to 1. General bounds are stated on this scale too. A general upper bound is stated as a position: by the 43/80 bound, for example, for large n there are words at position about 43/80 = 0.5375. The chart on the home page shows the shortest known word and the best lower bound at their positions. The page for each n gives lengths in letters, because there a single letter matters. ## How words are checked A contributor signed in with GitHub uploads a word as a file at /submit. For n from 3 through 9, it can be raw text or in the Detour format. For n from 10 through 14, Detour is required. The site then checks it in four steps. 1. The site reads the file and refuses a symbol outside the alphabet, a word that does not begin with the n symbols in order, and a length other than the one declared. 2. It refuses a word that is already verified, or whose mirror is. 3. Every word is checked by two streaming programs, using rotation classes (`classcheck`) and a bitmap of permutation ranks (`bitmapcheck`). Both must find every permutation and agree on their counts. The site also records repeated occurrences and computes the word's and mirror's hashes. It does not search for deletable letters or write the expanded word to disk. 4. A word shorter than the record when it was submitted, or a tie, is published as soon as both programs accept it. Any other word is published once the reason its submitter gave is approved. The section on submitting a word below has the sources of both programs and the exact commands the site runs, so you can check a word on your own computer before submitting it. Every verified word can be downloaded in Detour format, and words below n = 10 also as raw text. How to decode them is in the Detour section below. Apart from the historical results listed from the start, a bound is listed only with a Lean proof that the site checks itself. How to submit one is in the Lean section below. ## Points Contributors with at least 0.1 points are listed at /leaderboard, ranked by points. Each n from 6 to 14 is a prize of 100 points, and so is the coefficient of (n−3)! for large n. At a single n, the prize is the gap of (n−3)! letters between the 4chan bound and Egan's bound, counted on a log scale. A result that shrinks the gap at n from G letters to G′ letters earns 100 · ln((G + 1) / (G′ + 1)) / ln((n−3)! + 1) points, whether it lowers the upper bound or raises the lower bound. Closing the whole gap earns exactly 100. On this scale each letter is worth more than the one before it. At n = 7 the gap starts at 24 letters, and the last six letters earn 4.8, 5.7, 6.9, 8.9, 12.6 and 21.5 points, so the last letter at n = 7 is worth 21.5 points. For large n, the upper side starts at Egan's coefficient 1 and the lower side at 0, and moving either side by d earns 100d points. This scale is linear, because a log scale would never be used up. A general upper bound with coefficient 3/4, when the best had been 1, would earn 25 points. At each n from 6 to 14, upper-bound points require an actual word that passes the site's checks. A Lean proof that a word exists earns no points at that n and does not change the gap used for scoring. Its proved values are still shown, and its asymptotic coefficient can still earn points. Checked lower bounds still earn points at each n. A word generated from a historical existence proof is dated by the proof's first public date once that construction has been checked. Points come only from results a machine has checked: verified words, and bounds whose Lean proofs the site has checked. Each prize is split in half. One half is for every checked result, the other only for words and proofs checked in full by Lean's kernel. A proof that uses `native_decide` depends on compiled code that no kernel checks. It is reviewed by hand before it is listed, and it earns only the first half; the second half goes to the first kernel-checked proof of the same or a better bound. A proof of a custom statement, one that fits none of the site's fixed statements, is listed only after the statement is reviewed by hand, and then earns eligible points in full, or half if it uses `native_decide`. A result that is first on both counts earns all the points. The historical results listed from the start earn nothing. Results count in date order: words by their received time or announcement date, and bounds by when the site received their proofs, or by their announcement date if listed from the start. A result keeps its place in that order even when it is approved later, so an approval can move points from a later result to an earlier one. A result earns points only where it improves the best bound at that moment, so a word that ties the record earns nothing. Points at a given n come only from values at that n, and points for large n only from coefficients. Everyone credited for a result gets all of its points, and points do not decay. Results for n ≤ 5, where S(n) is known, are not scored. ## How to cite The records change, so cite a page by its address and the date you read it. For example: Jay Pantone, Superpermutation Almanac, https://superpermutations.com/n/13, accessed Nov 3, 2026. BibTeX: @misc{superpermutation-almanac, author = {Jay Pantone}, title = {The Superpermutation Almanac}, howpublished = {\url{https://superpermutations.com}}, note = {Accessed Nov 3, 2026}, year = {2026} } The data are licensed under CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/): you may reuse them with credit. Contact: Jay Pantone, jay.pantone@marquette.edu. ## The data Every page's data is also available as JSON: - /api/records: the shortest known word and best bounds at each n - /api/bounds: every listed bound with its evidence - /api/words (add ?n=13 for one n), and /api/words/W-0001 for one word - /api/leaderboard: the contributors and their points - /api/literature: every listed result, with sources and paper files - /api/events: the public change log; /feed.xml is the same as an Atom feed - /w/W-0001/download: a verified word as a Detour file; below n = 10, /w/W-0001/download/text gives raw text --- # Submitting a word A superpermutation is called a **word** here. ## What to upload - n can be 3 to 14. - For a word on n symbols, use the first n characters of `0123456789ABCD`. For example, n = 10 uses `0`–`9`, and n = 14 uses `0`–`9`, `A`, `B`, `C`, `D`. - The word must begin with the n symbols in order: `012` for n = 3, and `0123456789AB` for n = 12. If its first n letters are a permutation, relabelling the symbols always achieves this. - All letters go on one line, optionally followed by one newline and nothing else. The length is the number of letters, not counting that newline. - For n = 3 through 9, upload raw text or use the [Detour format](/docs/format) (`.detour`). For n = 10 through 14, a Detour file is required. The site tells the formats apart by their contents, not by the file name: renaming an ordinary `.xz` file to `.detour` does not convert it. - A Detour file must decompress within 128 MiB, and `detour encode` always writes files that do. - Files may be at most 200 MiB as uploaded. - A copy of a verified word is rejected, even if it is relabelled or read backwards. If your word uses letters 1..n, or numbers separated by commas or spaces, convert it with [convert_word.py](/tools/convert_word.py). It also relabels the symbols so that the word begins with them in order: ``` python3 convert_word.py my-word.txt word.txt ``` Below n = 10, you can upload `word.txt` directly or encode it as Detour. From n = 10 up, encode it as Detour; use your word's n in place of 10: ``` detour encode --n 10 word.txt word.detour ``` To install `detour`, see [the Detour format](/docs/format). The converter reads the whole word into memory, so for very large words (n ≥ 12), write the site's symbols directly, or relabel the word by streaming it through `tr` and the encoder. For n = 12 and n = 13: ``` # n = 12 head -c 12 word.txt # the first 12 letters, e.g. 3A0B12456789 tr "$(head -c 12 word.txt)" 0123456789AB < word.txt | detour encode --n 12 - relabelled.detour # n = 13 tr "$(head -c 13 word.txt)" 0123456789ABC < word.txt | detour encode --n 13 - relabelled.detour ``` A compressed word can be relabelled without writing it out uncompressed. For n = 13: ``` xz -dc word.txt.xz | head -c 13 # the first 13 letters xz -dc word.txt.xz | tr "$(xz -dc word.txt.xz | head -c 13)" 0123456789ABC | detour encode --n 13 - relabelled.detour ``` To relabel a Detour file, decode it, relabel the letters with `tr`, and encode them again. The site refuses a Detour file whose word does not begin with the n symbols in order, as it does any other file. ``` detour decode word.detour - | tr "$(detour decode word.detour - 2>/dev/null | head -c 13)" 0123456789ABC | detour encode --n 13 - relabelled.detour ``` At n = 14 the same pipe relabels the word without ever writing its 94 billion letters to disk: ``` detour decode word.detour - | tr "$(detour decode word.detour - 2>/dev/null | head -c 14)" 0123456789ABCD | detour encode --n 14 - relabelled.detour ``` ## Check before submitting Every word is stored as Detour and checked as a stream. The two coverage programs use different algorithms: rotation classes and a bitmap of permutations. Both must find every permutation and agree on the counts. The site also computes the word's hash, its mirror's hash and repeated occurrences. It does not search for deletable letters. Download [the Rust checkers](/tools/checkers-rs-source.tar.gz), build them, and replace `N` and `LENGTH` with the word's n and length: ``` tar xzf checkers-rs-source.tar.gz && cd checkers-rs && cargo build --release --locked ./target/release/classcheck N ../word.detour LENGTH ./target/release/wordhash N ../word.detour LENGTH ./target/release/bitmapcheck N ../word.detour LENGTH ``` Both coverage programs must report `"missing":0`. Memory needs grow with n; the full bitmap at n = 14 needs about 11 GB. These programs decode the Detour stream themselves, without writing the expanded word to disk. A `.detour` file is already xz-compressed, so upload it as it is. Plain xz-compressed text and gzip files are not accepted at any n. At n = 14 the site decodes at most half a byte of tokens per letter, plus 1 MiB. Below n = 14 the cap is four bytes per letter, plus 1 MiB. Re-encode files that exceed the cap with the standard encoder. ## What you are asked - **n** and **the length.** - **The file.** - **How you found it** (optional). Markdown, up to 5,000 characters. Put links and any tools or AI you used here. It is published after review. - **Why it is worth listing**, only if the word is longer than the current record. Such a word is listed as notable after review. A word of the same length as the record is a tie: it is listed at once, with no reason, up to 20 ties per person at each n. Beyond that, a tie needs a reason too. Submitting needs a GitHub account; the site asks GitHub only for your public profile. ## Limits - At most 3 words waiting to be uploaded or checked at a time. - At most 10 submissions in 24 hours, and at most 20 from one network. - The length must lie between the 4chan bound n! + (n−1)! + (n−2)! + n − 3 and Egan's bound, which adds (n−3)!. ## What happens next 1. Your file goes straight to storage, and the time it finishes arriving is recorded. When two discoveries are equal, the earlier time has priority. 2. The checker prepares the Detour file, computes its hashes, and runs both streaming coverage algorithms. Large words take longer; the submission status shows when checking finishes. 3. "My submissions" shows the result. A verified word appears in the record at once; its note appears after review. If a word fails, the reason is shown, for example a symbol at a given position or the permutations it misses. If the checker itself fails, the word is retried automatically, and the failure is never counted against you. --- # The Detour format A Detour file stores a superpermutation, called a **word** here, as the list of places where it leaves the walk of the recursive construction. Everything else is implied. Halfar's 6,747,917,464-letter word for n = 13 is 313 KB as a Detour file, against 35 to 90 MB as `.xz`. Detour files end in `.detour`. Any byte string can be stored as a Detour file, and decoding gives back exactly the same bytes, including a final newline. New word uploads at n = 10 through 14 must use Detour. At n = 3 through 9, raw text is also accepted. Plain xz-compressed text and gzip are not accepted at any n. The site stores every word as Detour. See [submitting a word](/submit) for the upload requirements. ## Steps A **window** is n consecutive letters of the word that are n distinct symbols, so a permutation. When the next window starts k letters after the current one, the word has taken a **step of weight k**: it dropped the window's first k letters and appended k new ones, which are the dropped letters in some order. For example, `012010210` is the recursive word for n = 3. Its windows are `012`, `120`, `201`, `102`, `021` and `210`, and its steps have weights 1, 1, 2, 1 and 1. The step from `201` to `102` drops `2` and `0` and appends `0` and `2`. The order of the k new letters is stored as a **rank**. The reference order is the dropped letters reversed, which is the recursive construction's choice, so that order has rank 0. For a step whose dropped letters are `d₁ … d_k`, write the reference list `d_k … d₁`. Then, for j = 0, 1, …, k − 1, take the position p_j (counting from 0) of the j-th new letter among the reference letters not yet used. The rank is Σ p_j · (k − 1 − j)!, so the first new letter's position is multiplied by (k − 1)!. A weight-1 step always has rank 0. ## The default step The recursive construction takes a predictable step at every point. Detour stores only the steps that differ from it, called **deviations**, and counts the rest. The rule uses n counters, c₁ … c_n, which start at 0 at the word's first window: - the default step has weight equal to the least k whose counter is below n − k, and rank 0; - if no counter is below its limit (as after the recursive word's n! − 1 steps), there is no default step, and every step is written as a deviation; - after any step of weight k, default or not, counter k goes up by 1, and every counter below k goes back to 0. So a run of n − 1 weight-1 steps goes once around a cycle of n windows. After that, the default is a weight-2 step, and so on. The recursive word for any n is one window followed by n! − 1 default steps, with no deviations. For n = 3, the counters run through the five steps above with defaults 1, 1, 2, 1, 1. ## The file A Detour file is one xz stream, with nothing after it, holding the **token stream**. A decoder accepts any xz stream that decompresses in at most 128 MiB of memory. An encoder should write LZMA2 with the settings of `xz -9e`, plus `lc=0`, `lp=0` and `pb=0`, and a CRC64 check. This command compresses a token stream that way: ``` xz --format=xz --check=crc64 --lzma2=preset=9e,lc=0,lp=0,pb=0 ``` Numbers are unsigned LEB128 varints (7 bits per byte, low bits first) unless their size is given. A varint must be in its shortest form: a decoder refuses one of two or more bytes whose last byte is `00`. - **Header.** - the bytes `DTR1`; - the version (1 byte), which is 1; - n (1 byte), from 2 to 16; - the n alphabet bytes, all different; - the sync exponent e (1 byte), from 0 to 40; 0 means no sync tokens. - **Tokens.** Each is G, the number of default steps to take first, then a code byte: | code | meaning | what follows | |---|---|---| | 0–152 | a step of weight k ≤ 5 and rank r, written as BASE[k] + r, with BASE = 0, 1, 3, 9, 33 for k = 1 to 5 | nothing | | 252 | a step of weight k from 6 to n | k (1 byte), then r | | 253 | literal bytes, copied to the output as they are | the count (at least 1), then the bytes | | 254 | a new window (START) | n bytes, a permutation of the alphabet | | 251 | a sync point (SYNC) | the output length so far (8 bytes, little-endian), the current window (n bytes), then the counters c₁ … c_n as n varints. Its G is always 0. | | 255 | the end (END) | nothing | - **Trailer.** The length of the decoded output (8 bytes, little-endian) and its SHA-256 (32 bytes). **Literals and new windows.** Bytes before the first window, between windows more than n letters apart, and after the last window are literals. A START follows each literal that is followed by a window, and it resets the counters. No step comes between a literal and the next START. **Sync points.** With e > 0, the encoder counts START, LIT and deviation tokens (not SYNC or END), starting from 0 at the first token. Right after writing a START or a deviation, if the count, including that token, has reached 2^e, it writes a SYNC token and sets the count back to 0. A SYNC never follows a literal directly; it waits for the next START. A SYNC repeats the decoder's state, so a long word can be decoded and checked in pieces. A decoder refuses a file whose SYNC tokens are not exactly where this rule puts them. `detour encode` uses e = 21 for n = 14. The site accepts any e within its token cap, but a small e can push a file over the cap, since each SYNC token adds more than 2n bytes. A decoder refuses a file that breaks any of these rules: - a step with no current window; - a token that equals the default step; - a missing SYNC, or one that does not match the decoder's state; - a trailer that does not match the decoded output; - any byte after the end. ## A worked example The word `012021` for n = 3 has windows `012`, `120` and `021`, so two steps: - weight 1, which is the default; - weight 2, which deviates, since the default after one weight-1 step is still weight 1. The token stream, in hexadecimal: ``` 44 54 52 31 01 03 30 31 32 00 header: DTR1, version 1, n = 3, alphabet 012, e = 0 00 fe 30 31 32 G = 0, START, the window 012 01 01 G = 1 (the weight-1 default step), then a weight-2 step of rank 0 00 ff G = 0, END 06 00 00 00 00 00 00 00 length 6 4c 89 c9 2a … 33 cb 0b the SHA-256 of 012021 ```

Decode to text

Every verified word can be downloaded as a Detour file, and words with n < 10 also as plain text. A `.detour` file is already xz-compressed; it is not encrypted. After installing the `detour` tool below, decode a downloaded file with: ``` detour decode W-0042.detour W-0042.txt ``` For large words, pipe the output directly into another program to avoid storing the full text: ``` detour decode W-0042.detour | YOUR_PROGRAM ``` The SHA-256 shown for a word excludes its optional final newline. The SHA-256 of the encoded file is the hash of the `.detour` file itself, so the two differ. ## Tools - **`detour`**, the site's encoder and decoder, written in Rust, with no unsafe code of its own. Decoding needs about 100 MB of memory, and encoding about 700 MB. Download [its source](/tools/detour-source.tar.gz) (MIT license), then build and install it with Rust 1.89 or later. `cargo install` puts `detour` in `~/.cargo/bin`, which a Rust installed with rustup has on the PATH: ``` tar xzf detour-source.tar.gz && cd detour && cargo install --path . --locked detour encode --n 13 word.txt word.detour detour decode word.detour word.txt detour info word.detour ``` `encode` uses the alphabet `0123456789ABCDEF` cut to n unless you give `--alphabet`. It reads standard input when no input file is given, so a word can be piped in without ever being written to disk: ``` xz -dc word.txt.xz | detour encode --n 13 - word.detour my-generator | detour encode --n 14 - word.detour ``` Each command prints a one-line JSON summary: the length, the SHA-256, and the steps and deviations by weight. `encode` and `decode` print it to standard error, so their output can be piped; `info` prints it to standard output. `encode --sync E` sets the sync exponent (by default 21 from n = 14 up, and 0 below); n can be 2 to 16. `decode` and `info` have no length limit unless you give `--max-length L`, which stops them once the word passes L letters, so give one for a file you do not trust. `--max-token-bytes B` also stops them once the token stream passes B bytes, which bounds their work: SYNC tokens write no letters, so the length alone does not. The site decodes an upload with both: L is the declared length plus 1, for a final newline, and B is 4 bytes for each of those letters plus 1 MiB below n = 14, and half a byte for each plus 1 MiB at n = 14. Below n = 14 a file without SYNC tokens always fits; at n = 14 a file `detour encode` wrote always fits, since real words need 0.03 to 0.23 bytes a letter. An n = 13 word takes about two and a half minutes to encode and under two minutes to decode. - **[reference.py](/tools/detour_reference.py)**, a second encoder and decoder in about 350 lines of Python, written independently of the Rust tool. It agrees with it on every test file. It is slow, about a million letters a second, but short enough to read and check. ## Instructions for agents To produce a Detour file of a word: 1. Get the word's letters as a byte stream, by reading a file or by running the program that builds the word. Never write a large word to disk uncompressed if you can pipe it. 2. Pipe the stream into `detour encode --n N - OUT.detour`. For the site's alphabet, give no `--alphabet`. 3. Run `detour info OUT.detour`. Its `length` must be the word's length in letters (plus 1 if the stream ended with a newline), and its `sha256` must be the SHA-256 of the stream. 4. Report the length and the SHA-256 together with the file. --- # Lean proofs [Submit a Lean proof](/lean/submit) · [Templates and codes as JSON](/lean/templates.json) Apart from words, bounds can be submitted only as Lean proofs, which the site checks itself. A submission is one commit of a public GitHub repository. The file `AlmanacSolution.lean` at its root states the results, one theorem per result, each proved by a theorem from your project. A result uses one of the Almanac's [templates](#templates) or is a [custom statement](#custom-statements). The site copies the repository, builds it once on a machine with no secrets, and checks each result with two independent kernels, Lean's own and NanoDa. To submit, use [the form](/lean/submit). Each heading's anchor is in braces after it. ## Quick start {#quick-start} 1. Make a branch in a public GitHub repository under your own account, not a fork. Organization repositories aren't supported yet. The branch can be a temporary one that collects the parts of a larger project you need (see [Monorepos](#monorepos)). 2. At the root of the branch, put a Lake project: `lean-toolchain` with `leanprover/lean4:v4.35.0`, a `lakefile.toml` that declares the four Almanac libraries, `lake-manifest.json` if the project has dependencies, and `AlmanacSolution.lean`. The [scaffold](/lean/batch-scaffold.zip) has all of these, and the [example project](/lean/batch-example.zip) is a complete batch that builds. 3. In `AlmanacSolution.lean`, state each result as one theorem inside `namespace AlmanacSubmission`, using a [template](#templates) type wherever one fits. 4. Run `lake build AlmanacSolution` and check the axioms ([Checking before you submit](#checking-locally)). 5. Push the branch. On [the form](/lean/submit), enter the repository (or choose it from the list of your repositories) and a branch, tag or commit, and read the preview: each statement, what it would change, the estimated points, and any problems, with how to fix each. 6. Set the authors, tick the box giving the Almanac permission to host the commit's files ([Source retention](#source-retention)), and submit. The site checks the previewed commit even if the branch moves later. 7. Keep the branch until [My submissions](/me) shows the submission as **Archived**. After that the site has its own copy, and you can delete the branch. Sign in with GitHub to preview and submit. An account can have one submission being checked at a time and can send 5 submissions in 24 hours; a batch of up to 24 results counts as one. For now, batches are checked only on the site's hosted machines. New submissions require **Lean v4.35.0** (`leanprover/lean4:v4.35.0`). If you use Mathlib, pin commit `56a005855ea17e0b0958f73ec801ae140b0a1679`. These older environments are retained for historical proofs and rechecks: - Lean v4.30.0, with Mathlib at commit `c5ea00351c28e24afc9f0f84379aa41082b1188f` - Lean v4.31.0, with Mathlib at commit `fabf563a7c95a166b8d7b6efca11c8b4dc9d911f` ## What is listed, and what scores {#listing} The statements in a batch are separate results, each with its own outcome. - A template statement with a kernel-checked proof is listed as soon as the judge accepts it, and earns its eligible points in full. Its only axioms may be `propext`, `Classical.choice` and `Quot.sound`. - A proof that uses `native_decide` is listed only after it is reviewed by hand, and earns half the eligible points. The other half goes to the first kernel-checked proof of the same or a better bound. See [Native and custom proofs](#native-and-custom). - A custom statement is listed after its mathematical interpretation is reviewed and approved. It earns its eligible points in full when kernel-checked, or half when it uses `native_decide`. - Nothing else counts as a result: not a paper, a preprint, a certificate or a written proof, nor Lean that the judge refused or could not run. A template result is accepted only if it improves the best machine-checked bound at some n from 3 to 14, or the coefficient of (n−3)! or (n−4)! for large n, or if it is the first kernel-checked proof of a bound that so far only a `native_decide` proof gives. Ties are not listed. The form refuses a batch if any result improves nothing or contradicts a public result or another result in the batch. A custom statement gets the same test when its interpretation is approved. All results in a batch are dated by when the site received the batch, not by the commit, and a result received earlier has priority. At a single n, upper-bound points require a checked word; a proof that a word exists earns no points at that n. The coefficient of (n−4)! has **no points prize**: an improvement there is listed but earns no points. The scoring rule is under [How points work](/docs/points). ## Files at the root {#file-layout} At the submitted commit, the root of the repository has these files: ``` lean-toolchain leanprover/lean4:v4.35.0 lakefile.toml the four Almanac libraries and your own lake-manifest.json if the project has dependencies AlmanacSolution.lean your results, one theorem each AlmanacDefs.lean the Almanac's definitions (the judge writes its own copy) AlmanacStatement.lean a placeholder (the judge writes its own) AlmanacChallenge.lean a placeholder (the judge writes its own) YourProject/… your proofs paper/ an optional write-up, PDF and TeX (see Papers) ``` Besides your own libraries, `lakefile.toml` declares four libraries, `AlmanacDefs`, `AlmanacStatement`, `AlmanacChallenge` and `AlmanacSolution`, each with only its name and no `srcDir`. The judge overwrites any `AlmanacDefs.lean`, `AlmanacStatement.lean` and `AlmanacChallenge.lean` with its own, so your copies matter only when you build the proof yourself. A batch does not use `AlmanacStatement` or `AlmanacChallenge`; the judge builds its Challenge from the statements in `AlmanacSolution.lean`. Both placeholder libraries must still be declared in `lakefile.toml`; the scaffold declares both. The project must also follow these rules: - Use a declarative `lakefile.toml` at the root and in every dependency outside Mathlib's ecosystem, with exactly `lakefile.toml` and `lake-manifest.json` at the dependency's root (no `subDir`). A TOML lakefile runs no code, so nothing you wrote runs while the network is on. - Dependencies must be git repositories on github.com, each pinned to a full commit in `lake-manifest.json`. Path dependencies are not allowed. - If you use Mathlib, its address must be exactly `https://github.com/leanprover-community/mathlib4`, without `.git` at the end, in both `lakefile.toml` and `lake-manifest.json`. The packages Mathlib depends on must have the addresses and commits from Mathlib's own `lake-manifest.json` at the pinned commit. If you start from the scaffold's `lakefile.toml`, `lake update` sets all of these correctly. - No external code: no `--load-dynlib`, `moreLinkArgs` or extern libraries, and no committed binaries or object files. Sources in other languages may be present but are never built. Lake's `precompileModules` is allowed. - No module may be named `Init`, `Std`, `Lean` or `Lake`, in your repository or in a dependency. - Every committed Lean file in your repository has at most 10,000 lines, and the repository with its dependencies, other than Mathlib's, is at most 500 MiB at that commit. You can download: - [The scaffold](/lean/batch-scaffold.zip), version 4: a root project with a commented `lakefile.toml` and `AlmanacSolution.lean`, the three judge files and the required `lean-toolchain`. - [The example project](/lean/batch-example.zip): a complete batch that builds, with one template statement and one custom statement, both about S(3). The 4chan bound already gives S(3) ≥ 9, so the preview reports `NO_IMPROVEMENT` and the form will not submit it, but it shows the layout and you can run the checks below on it. Or download its files separately: [AlmanacSolution.lean](/lean/batch-example/AlmanacSolution.lean), [ExampleProject.lean](/lean/batch-example/ExampleProject.lean), [S3.lean](/lean/batch-example/S3.lean), [lakefile.toml](/lean/batch-example/lakefile.toml). - [AlmanacDefs.lean](/lean/AlmanacDefs.lean), the definitions ([below](#definitions)). The scaffold's `lakefile.toml` follows, for an agent that cannot unpack the download. If you use Mathlib, uncomment the `[[require]]` lines, which pin the required commit: ```toml # The root Lake project of a Superpermutation Almanac batch submission. name = "almanac_submission" # The four reserved Almanac libraries, with their files at the repository root: each has only its name # and no srcDir. The judge overwrites AlmanacDefs.lean, AlmanacStatement.lean and AlmanacChallenge.lean # with its own, so your copies matter only for your own builds. AlmanacStatement and AlmanacChallenge are # placeholders that a batch does not use; the judge builds its Challenge from the statements in # AlmanacSolution.lean. [[lean_lib]] name = "AlmanacDefs" [[lean_lib]] name = "AlmanacStatement" [[lean_lib]] name = "AlmanacChallenge" [[lean_lib]] name = "AlmanacSolution" # Your own library: rename MyResults, and add one [[lean_lib]] for each of your libraries. [[lean_lib]] name = "MyResults" # With Mathlib, uncomment these lines, run `lake update` so that lake-manifest.json pins it, and commit # lake-manifest.json too. # [[require]] # name = "mathlib" # git = "https://github.com/leanprover-community/mathlib4" # rev = "56a005855ea17e0b0958f73ec801ae140b0a1679" ``` The example's `AlmanacSolution.lean`: ```lean -- The Almanac's example batch: one recognized template and one custom statement, both about S(3). -- The 4chan bound already gives S(3) ≥ 9, so the preview shows that this adds no new record. import AlmanacDefs import ExampleProject namespace AlmanacSubmission /-- S(3) ≥ 9, stated with the template Almanac.LowerBoundAt. -/ theorem lower_three : Almanac.LowerBoundAt 3 9 := ExampleProject.lower_three /-- A custom statement: no word of length 8 on three symbols contains every arrangement. -/ theorem short_words_miss : ExampleProject.ShortWordsMiss := ExampleProject.short_words_miss end AlmanacSubmission ``` and its `ExampleProject.lean`, which proves both results from `S3.lean`: ```lean import S3 /-! The example batch's own results: S(3) ≥ 9 from the check over all short words in S3.lean, and a custom statement about that same check. Nothing here is new. -/ namespace ExampleProject /-- No word of length 8 on three symbols contains all six arrangements, checked by the kernel. -/ theorem no_cover_8 : (S3.allWords 8).all (fun w => !S3.coversB w) = true := by decide +kernel /-- S(3) ≥ 9: the proof of the template statement `lower_three`. -/ theorem lower_three : Almanac.LowerBoundAt 3 9 := S3.lowerBound_of 8 no_cover_8 /-- The type of the custom statement `short_words_miss`: every word of length 8 on three symbols misses an arrangement. -/ abbrev ShortWordsMiss : Prop := (S3.allWords 8).all (fun w => !S3.coversB w) = true theorem short_words_miss : ShortWordsMiss := no_cover_8 end ExampleProject ``` ## The entry file {#entry-file} The site reads `AlmanacSolution.lean` before anything is built, so the file has a small fixed form: ```text file = { import } , { moddoc } , namespace , { item } , end , EOF import = "import" , MODULE (MODULE on the same line) namespace = "namespace" , "AlmanacSubmission" (the name on the same line) item = moddoc | [ doc ] , wrapper wrapper = "theorem" , NAME , ":" , TYPE , ":=" , proof proof = REF | "by" , "exact" , REF end = "end" , "AlmanacSubmission" (the name on the same line; only comments may follow) ``` - Imports come first, one per line, with only comments before them. No `open`, `set_option`, `variable` or declaration may come before the namespace, and the file may not import `AlmanacChallenge` or `AlmanacSolution`. - `NAME` is a simple ASCII identifier of letters, digits and underscores that starts with a letter or underscore, has at most 64 characters and is not a Lean keyword. No name may be used twice. - `TYPE` is everything up to the first `:=` outside brackets, and may span several lines. A top-level `let` must be in parentheses. - The proof is the fully qualified name of one theorem from an imported module, written `Name` or `by exact Name`. If that theorem needs arguments, or a bridge to the type, write a [linking lemma](#linking-lemmas) in your project. - Nothing else goes in the namespace: no `lemma`, `def`, `instance`, attributes, `open`, sections, notation or commands. A doc comment (`/-- … -/`) may come just before a wrapper, and module docs between wrappers. - The file has at most 24 wrappers and at most 256 KiB. Each theorem in the namespace is a *wrapper*: it states one result and is proved by a theorem from your project. The rest of this page calls wrappers statements. There are three kinds: ```lean import AlmanacDefs import ExampleProject.Results namespace AlmanacSubmission -- A template: recognized automatically, compared with the Almanac's own statement. theorem lower_example : Almanac.LowerBoundAt 3 9 := ExampleProject.lower_example -- A custom statement with an explicit type: reviewed by hand. theorem custom_explicit : ∀ n : Nat, 3 ≤ n → ExampleProject.SomeBound n := ExampleProject.some_bound -- A custom statement with an inferred type: also reviewed by hand, and it stays custom. theorem custom_inferred : type_of% ExampleProject.big_theorem := ExampleProject.big_theorem end AlmanacSubmission ``` These names are schematic; the example project above is the one that builds. Lean requires a type after a theorem's name, so `theorem x := Foo.bar` is refused (`THEOREM_TYPE_REQUIRED`). With `type_of% Fully.Qualified.theorem` you can submit a theorem without restating its type, but the statement is then custom for good, even if its type turns out to be a template. To have a statement recognized automatically, write the template type. Keep AlmanacSolution.lean in plain Lean syntax; if your imports change how it parses, the preview may differ and the build will be refused. The preview parses the file with Lean's built-in grammar and does not know notation defined by your imports. In the few places where such notation could change how Lean reads the file, plain text is required: - A name that ends in a command word, such as `l.append` (which ends in `end`), may not directly follow a symbol other than Lean's own brackets and operators (`TOKEN_ADJACENT`). Mathlib's norm `‖l.append m‖` is the usual case: write `‖ l.append m‖`. The same holds for a comment or `«` directly after another token. - String, character and name literals (`"x"`, `'c'`, `` `foo ``) are refused (`LITERAL_UNSUPPORTED`). If a type needs one, make it a definition in one of your modules and use that definition as the statement's type. The preview only reads the source. After the build, the judge lists every theorem that the compiled `AlmanacSolution` module declares in the namespace, and refuses the build if they differ from the previewed ones. So nothing is listed that the preview did not show. ## Templates {#templates} A template statement's type is a template applied to its parameters and nothing else: no hypotheses, no conjunctions, no surrounding parentheses. `open` does not work for templates, so always write the `Almanac.` prefix. Write the parameters in canonical form, the text the judge uses in its own Challenge, so that the compiled statements can be compared exactly: - **A natural literal** (`n`, `v`, `n0`, `n1`, `k`) is decimal digits with no sign, separator, leading zero or parentheses: `3`, `33`. - **A rational** (`c`) is at least 0 and in lowest terms: an integer such as `5` or `0`, or a fraction in parentheses such as `(7/2)`. `(5)`, `(10/2)` and `3.5` are refused, with the canonical text to paste. `7/2` without parentheses is three arguments, which makes the statement custom. - **A formula** (`f`) is an `Almanac.Expr` constructor term exactly as the site writes it: `(.const 5)`, `(.const (-5))`, `(.const (1/3))`, `(.var)` for n, `(.pow j)` for nʲ, `(.fact k)` for (n−k)!, and `(.add a b)`, `(.sub a b)`, `(.mul a b)`, `(.div a b)`. You may write `Almanac.Expr.add` for `.add`. Line breaks, extra spaces and comments are allowed, but a space is required wherever the canonical text has one. Each factorial's k must be at most n₀, and each divisor must be positive for n ≥ n₀. For example, n! + (n−1)! + (n−2)! + n − 3 is ```lean (.sub (.add (.add (.add (.fact 0) (.fact 1)) (.fact 2)) (.var)) (.const 3)) ``` If a parameter is written another way, the preview shows the canonical type to paste (`TEMPLATE_PARAMETER_NONCANONICAL`). The targets are each n from 3 to 14, scored at n = 6 to 14; the coefficient of (n−3)! for large n, which is scored; and the coefficient of (n−4)! for large n, which has no points prize. A statement about one factorial scale counts for nothing at another, even when the mathematics implies a bound there. State each consequence you want listed as a separate template statement, with a linking lemma for it. ### Almanac.LowerBoundAt n v {#template-lower-at} Every superpermutation on n symbols has length at least v. - Parameters: `n`, a natural literal from 3 to 14; `v`, a natural literal from 1 to 10¹⁵. - Scope: One n. - Template id `lower_at`, version 1.0.0. ```lean def LowerBoundAt (n v : Nat) : Prop := ∀ w : Word n, IsSuperpermutation n w → v ≤ w.length ``` Example, not a result: ```lean theorem lower_at_example : Almanac.LowerBoundAt 3 9 := ExampleProject.lower_at_example ``` ### Almanac.LowerBoundFrom n0 f {#template-lower-from} For every n ≥ n₀, every superpermutation on n symbols has length at least f(n). - Parameters: `n0`, a natural literal from 1 to 10¹⁸; `f`, a formula of at most 200 constructors. - Scope: Every n ≥ n₀. The preview shows its values at n = 3 to 14, and its consequence for the coefficient of (n−3)! (and of (n−4)!) when the site can derive one from the formula. - Template id `lower_from`, version 1.0.0. ```lean def LowerBoundFrom (n₀ : Nat) (f : Expr) : Prop := ∀ n : Nat, n₀ ≤ n → ∀ w : Word n, IsSuperpermutation n w → f.eval n ≤ (w.length : Rat) ``` Example, not a result: ```lean theorem lower_from_example : Almanac.LowerBoundFrom 3 (.add (.add (.fact 0) (.fact 1)) (.fact 2)) := ExampleProject.lower_from_example ``` ### Almanac.LowerBoundRange n0 n1 f {#template-lower-range} For n₀ ≤ n ≤ n₁, every superpermutation on n symbols has length at least f(n). - Parameters: `n0`, a natural literal from 1 to 10¹⁸; `n1`, a natural literal from n₀ to 10¹⁸; `f`, a formula of at most 200 constructors. - Scope: Each n from n₀ to n₁, and nothing about large n. - Template id `lower_range`, version 1.0.0. ```lean def LowerBoundRange (n₀ n₁ : Nat) (f : Expr) : Prop := ∀ n : Nat, n₀ ≤ n → n ≤ n₁ → ∀ w : Word n, IsSuperpermutation n w → f.eval n ≤ (w.length : Rat) ``` Example, not a result: ```lean theorem lower_range_example : Almanac.LowerBoundRange 3 5 (.fact 0) := ExampleProject.lower_range_example ``` ### Almanac.UpperBoundFrom n0 f {#template-upper-from} For every n ≥ n₀ there is a superpermutation on n symbols of length at most f(n). - Parameters: `n0`, a natural literal from 1 to 10¹⁸; `f`, a formula of at most 200 constructors. - Scope: Every n ≥ n₀. Upper bounds at a single n earn points only with a verified word, so with this template, points come only from the coefficient of (n−3)!. - Template id `upper_from`, version 1.0.0. ```lean def UpperBoundFrom (n₀ : Nat) (f : Expr) : Prop := ∀ n : Nat, n₀ ≤ n → ∃ w : Word n, IsSuperpermutation n w ∧ (w.length : Rat) ≤ f.eval n ``` Example, not a result: ```lean theorem upper_from_example : Almanac.UpperBoundFrom 3 (.mul (.const 2) (.fact 0)) := ExampleProject.upper_from_example ``` ### Almanac.AsymptoticUpper c {#template-asymptotic-upper} For every ε > 0, for all large n, some superpermutation on n symbols has length at most n! + (n−1)! + (n−2)! + (c + ε)(n−3)!. - Parameters: `c`, a rational at least 0, numerator and denominator of at most 12 digits. - Scope: Large n, at the scale (n−3)!, with no finite consequence. - Template id `asymptotic_upper`, version 1.0.0. ```lean def AsymptoticUpper (c : Rat) : Prop := ∀ ε : Rat, 0 < ε → ∃ N : Nat, ∀ n : Nat, N ≤ n → ∃ w : Word n, IsSuperpermutation n w ∧ (w.length : Rat) ≤ asymptoticForm n (c + ε) ``` Example, not a result: ```lean theorem asymptotic_upper_example : Almanac.AsymptoticUpper 5 := ExampleProject.asymptotic_upper_example ``` ### Almanac.AsymptoticLower c {#template-asymptotic-lower} For every ε > 0, for all large n, every superpermutation on n symbols has length at least n! + (n−1)! + (n−2)! + (c − ε)(n−3)!. - Parameters: `c`, a rational at least 0, numerator and denominator of at most 12 digits. - Scope: Large n, at the scale (n−3)!, with no finite consequence. - Template id `asymptotic_lower`, version 1.0.0. ```lean def AsymptoticLower (c : Rat) : Prop := ∀ ε : Rat, 0 < ε → ∃ N : Nat, ∀ n : Nat, N ≤ n → ∀ w : Word n, IsSuperpermutation n w → asymptoticForm n (c - ε) ≤ (w.length : Rat) ``` Example, not a result: ```lean theorem asymptotic_lower_example : Almanac.AsymptoticLower 0 := ExampleProject.asymptotic_lower_example ``` ### Almanac.AsymptoticUpperAt k c {#template-asymptotic-upper-at} For every ε > 0, for all large n, some superpermutation on n symbols has length at most n! + (n−1)! + (n−2)! + (c + ε)(n−k)!; k is 3 or 4. - Parameters: `k`, a natural literal 3 or 4; `c`, a rational at least 0, numerator and denominator of at most 12 digits. - Scope: Large n, at the scale (n−k)!, with no finite consequence and nothing at any other scale. With k = 3 it is AsymptoticUpper c. - Points: k = 3 scores as the (n−3)! coefficient; k = 4 has no points prize. - Template id `asymptotic_upper_at`, version 1.0.0. ```lean def AsymptoticUpperAt (k : Nat) (c : Rat) : Prop := ∀ ε : Rat, 0 < ε → ∃ N : Nat, ∀ n : Nat, N ≤ n → ∃ w : Word n, IsSuperpermutation n w ∧ (w.length : Rat) ≤ asymptoticFormAt k n (c + ε) ``` Example, not a result: ```lean theorem asymptotic_upper_at_example : Almanac.AsymptoticUpperAt 3 5 := ExampleProject.asymptotic_upper_at_example ``` ### Almanac.AsymptoticLowerAt k c {#template-asymptotic-lower-at} For every ε > 0, for all large n, every superpermutation on n symbols has length at least n! + (n−1)! + (n−2)! + (c − ε)(n−k)!; k is 3 or 4. - Parameters: `k`, a natural literal 3 or 4; `c`, a rational at least 0, numerator and denominator of at most 12 digits. - Scope: Large n, at the scale (n−k)!, with no finite consequence and nothing at any other scale. With k = 3 it is AsymptoticLower c. - Points: k = 3 scores as the (n−3)! coefficient; k = 4 has no points prize. - Template id `asymptotic_lower_at`, version 1.0.0. ```lean def AsymptoticLowerAt (k : Nat) (c : Rat) : Prop := ∀ ε : Rat, 0 < ε → ∃ N : Nat, ∀ n : Nat, N ≤ n → ∀ w : Word n, IsSuperpermutation n w → asymptoticFormAt k n (c - ε) ≤ (w.length : Rat) ``` Example, not a result: ```lean theorem asymptotic_lower_at_example : Almanac.AsymptoticLowerAt 4 0 := ExampleProject.asymptotic_lower_at_example ``` ## Custom statements {#custom-statements} A statement whose type is not exactly a template is a custom statement. Its proof is checked like any other, with both kernels and the same rules for axioms and `native_decide`. The judge then extracts the theorem's complete type, with every definition it uses, from the checked export. A model compares that statement with a proposed mathematical interpretation, and the interpretation is reviewed by hand before the result is listed. The result's page is flagged "statement reviewed, not matched to a fixed statement." Until then its effect is unknown, so the preview leaves it out of the points estimate. For now, an approved custom statement is listed only with consequences at single n and for the coefficient of (n−3)!. A result about the coefficient of (n−4)! needs a template statement: `Almanac.AsymptoticUpperAt` or `Almanac.AsymptoticLowerAt` with k = 4. A custom statement is meant for a theorem that fits no template. When a template fits, make the statement one that is recognized automatically: - Write the template type. `theorem w : Almanac.LowerBoundFrom 6 (…) := MyProject.w` is recognized; `theorem w : type_of% MyProject.w := MyProject.w` is not, whatever `MyProject.w` says. - If your theorem uses your own definitions, prove the template in your project with a [linking lemma](#linking-lemmas), and use that lemma as the statement's proof. - Split conditions and conjunctions. A type with a hypothesis, or `A ∧ B`, is custom (`TEMPLATE_HEAD_NOT_EXACT`). State each unconditional consequence separately, with a linking lemma for each. An exact limit of the coefficient is two statements, `AsymptoticUpperAt k c` and `AsymptoticLowerAt k c`. - Put binders after the colon. `theorem w (n : Nat) : P n` is refused (`BINDERS_UNSUPPORTED`); `theorem w : ∀ n : Nat, P n` is a custom statement. - Move literals into a definition. A type with a string or character literal must be a `def` in your project (`LITERAL_UNSUPPORTED`). A checked proof of `True`, or of a theorem that assumes its conclusion, does not establish a bound or earn points. The extracted statement may be at most 1.8 MB; a larger one goes to the review queue as over a limit. ## Linking lemmas {#linking-lemmas} A linking lemma restates a theorem of your project with exactly the type a statement needs. Put it in one of your own modules, prove it there, and use its name as the statement's proof: ```lean -- In ExampleProject/Links.lean (schematic): import AlmanacDefs import ExampleProject.Main theorem ExampleProject.lower_four : Almanac.LowerBoundAt 4 33 := by intro w hw exact ExampleProject.main_bound 4 w (ExampleProject.isSuper_of_almanac hw) ``` Adding a type annotation does not prove that two statements are equivalent. If your theorem uses your own definition of superpermutations or of length, the linking lemma must prove that it agrees with the Almanac's `IsSuperpermutation` and `List.length`, and the judge checks that proof like any other. Specialize a theorem that takes arguments (`main_bound n`) in the linking lemma, never in the statement. A statement's proof must be a name, so `:= Foo.bar 7` and `:= by simpa using Foo.bar` are refused (`PROOF_REFERENCE_UNSUPPORTED`). ## Monorepos {#monorepos} The project must be at the root of the submitted commit; a subdirectory cannot be chosen. If your results are part of a larger repository, make a submission branch whose root `lakefile.toml` declares the Almanac libraries and the libraries the results need, and whose `AlmanacSolution.lean` imports only those modules. Every dependency must be pinned to a full commit in `lake-manifest.json` and follow the same rules as the root. Narrow imports make the build faster, but they do not narrow the checks. The source rules for `native_decide` cover every Lean file in your repository and in its dependencies outside the pinned Mathlib ecosystem, including files that nothing imports. If part of a monorepo has code that a native proof may not contain, leave it off the submission branch. ## Reading the preview {#preview} For the commit you enter, the preview shows: - Whether `AlmanacSolution.lean` was found, the commit it was read from (the commit a submission checks, even if the branch moves), and the number of statements. - Each statement's name and line, marked **Recognized template**, with the claim typeset, or **Custom statement**, with its type and line numbers. Proofs are checked only after you submit. - For each target a claim improves, one line with the interval given by all checked results now, in gray, and with the claim, in black, and a table of values at each n under the statement. The coefficient of (n−3)! is drawn from 0 to 1. A target with no known upper end is shown one-sided. Where the kernel-checked results alone give a different interval, that interval is shown too. - Estimated points. Proofs using `native_decide` earn half the points. The batch total counts all the results together, so a result that follows from another in the batch adds nothing. Custom statements are left out. - The caveat "Points are estimated from results accepted so far, and can change if an earlier submission still being checked is accepted." and the number of earlier submissions still being checked, with nothing else about them. Some results improve the listed bounds but earn no points: results at n = 3 to 5, finite upper bounds proved without a word, and the coefficient of (n−4)!. If two results in a batch give the same best value with different authors, the points for that value wait until the credit is reviewed. A full commit SHA must be on a branch or tag of the repository, because GitHub also shows a fork's commits at the original repository's address. If it is not, give a branch or tag that has it; tag the commit or push it to a branch if none does. A preview is valid for 15 minutes. Changing the repository or the ref makes it stale until the new one is read. If the branch moves after the preview, the site still checks the previewed commit, and you can read the new one instead. You can preview 10 times a minute and 60 times an hour, counted per account and per IP address. Everyone who previews shares the site's allowance of GitHub requests (the site may use a read-only token of its own). When GitHub's limit is reached, the preview shows when to try again; nothing is wrong with your source. ### The preview's format {#preview-format} The form's live preview is `POST /lean/submit/preview`, sent from a signed-in session with its CSRF token. The fields are `repository`, `ref` (blank for the default branch), `authors`, and for each statement `override_NAME` and `authors_NAME`, with an optional `request_id` that is echoed back and `refresh=1` to resolve a branch again. The answer is JSON with the schema `almanac-batch-preview/1`: - the versions; - `state`: `ready`, `retry` or `blocked`; - `source`: the canonical repository, ref, full commit, entry path and SHA-256; - `compatibility`; - `wrappers`: ordinal, name, span, classification, source mode, ClaimSpec, canonical type, values at n = 3 to 14 as text, type excerpt, reference, authors and problem codes; - `counts` and `catalogue_sha256`; - `impact` (`almanac-batch-impact/1`): for each claim and for the batch, the interval of every target now and in each scenario, and the points; - `paper`: the files taken from `paper/` (path, size, git object id and media type), their total and digest, and the first files left out with the reason; null if there is no `paper/` folder; - `problems`: code, severity, blocking, retryable, message, repair, location and anchors; - the preview token and its expiry. Every value that can exceed 2⁵³ is text. [templates.json](/lean/templates.json) lists the templates, targets and codes in the same terms. A target's `baseline` there is the interval given by the classical formula bounds (the 4chan bound and Egan's), not the current record; the listed bounds are at [/api/bounds](/api/bounds). An agent usually checks the entry file locally instead, and leaves the preview on the form to the author. ## Authors {#authors} The authors list on the form applies to every statement in the batch, and starts with you. Write one author per line: `@` and a GitHub username, or a name. To give a statement a different list, open **Change authors** under it. A statement you do not change uses the shared list, and later changes to the shared list do not affect a statement you changed. You are credited, with your GitHub account, only if you are on a list; submitting someone else's proof does not make you an author. Every other author is reviewed before their credit appears. Until a result has an approved author, it shows **Credits pending review** and earns no one points; the submitter does not get them by default. The result keeps its date when the authors are approved. ## Native and custom proofs {#native-and-custom} A batch is built once. Its results are then checked in two groups, proofs without `native_decide` and proofs with it, which are exported and replayed separately: - A kernel-checked template result is listed as soon as it passes, without waiting for anything else in the batch. - A template result whose proof uses `native_decide` waits for review, and earns half. - A custom statement waits for review of its interpretation, however its proof is checked. If the build fails, the whole batch fails. After the build, the two groups are judged independently. A problem in one group, such as code anywhere in the project that a `native_decide` proof may not contain, refuses that group's results and not the other's. Within a group, each result passes or fails on its statement and axioms. ### native_decide {#native-decide} `native_decide` proves a statement by compiling and running a computation. The judge runs that computation again and checks the rest of the proof with both kernels, but no kernel checks the computation itself. Such a proof is reviewed by hand before it is listed, with a note explaining this, and earns, where eligible for points, half the kernel-checked rate. A proof using `native_decide` must not run its own metaprograms or effectful callbacks during the build. This rule covers all your Lean source files and all dependencies outside the pinned Mathlib ecosystem, including files the final proof does not import. Ordinary computational definitions are allowed. The rule excludes evaluation commands such as `#eval`, `run_cmd`, `run_meta` and `run_elab`; `run_tac` and `by_elab`; your own tactics, elaborators, macros, parsers and simprocs; and initialization code. The excluded simprocs include CBV and symbolic procedures, and generated simp-set attributes whose names end in `_proc`. Declarations made with `syntax`, `declare_syntax_cat` and `binder_predicate` are excluded too. The judge checks both the source and the registrations in the compiled Lean environment. `notation`, `infix`, `infixl`, `infixr`, `prefix` and `postfix` are allowed, and so are the tactics and notation of the pinned Lean and Mathlib. The restrictions on unsafe code, replacement compiled implementations, foreign code, extra axioms and `sorry` still apply. The rule also excludes registering your own extensions with `@[try_suggestion]`, `@[norm_num]`, `@[positivity]`, `@[aesop]` or docstring handler attributes, and defining your own pretty printers, library-suggestion or missing-documentation handlers, Inclusion extensions, or Do or Grind elaborators. `set_library_suggestions` and `postprocess_traces` may not install or run your own callbacks. The library's `norm_num`, `positivity`, `aesop`, `simp`, `cbv` and `grind` tactics are allowed. Aesop's `(add ...)` option can register a custom tactic, so it is excluded too. The source scan refuses any parenthesized expression that starts with the bare name `add`. If this catches an ordinary function call, qualify the name, as in `(Nat.add x y)`, or rename the function. Some tactic configurations can contain executable callbacks. To keep them out, the scan refuses, for native proofs, parenthesized assignments to `config`, `oracle`, `preprocessors`, `discharger`, `proc`, `suspend`, `discharge`, `toBacktrackConfig` or `toSolveByElimConfig`, including qualified or quoted field names and subfields. This also refuses pure whole configurations and ordinary named arguments with these names. Plain library tactics are still available, and so are individual pure options with other names, such as `linarith (splitHypotheses := true)`. A proof checked in full by the kernels can use these configurations. ### Strings and interpolation {#strings} String interpolation puts ordinary Lean expressions in braces, and those expressions can contain constructs such as `by_elab` that run code during elaboration. A parser can request interpolation without an `s!` prefix, so the source scan checks possible brace expressions in every ordinary string, including strings in notation declarations. It refuses a string when nested quotes, an unmatched opening brace or deep nesting make this ambiguous, even if the string was meant literally. Use a raw string for literal braces, such as `r#"{literal text}"#`, and raw token strings for brace notation: `notation r"{" x r"}" => x`. If an interpolated expression contains quotes, move it into a separate definition and interpolate its name. Comments and raw strings are not scanned. These source restrictions do not apply to proofs checked in full by the kernels. ## Source retention {#source-retention} Every batch gives the Almanac permission to keep and publicly host all files of its commit as a permanent record. The form has a box for this above the submit button, and a batch cannot be submitted without it. After you submit, the site copies the repository at the previewed commit, and each dependency outside Mathlib's ecosystem, into the site's storage, as compressed git packs of exactly one commit each. The judge builds only this copy, never GitHub's. When the copy is complete, [My submissions](/me) shows the submission as **Archived**, and you may delete the branch. A listed result's page links to the copy and to the commit on GitHub. To unpack a copy: ``` git init copy && cd copy zstd -dc ../0-repository.pack.zst | git index-pack --stdin echo COMMIT > .git/shallow && git checkout COMMIT ``` The site keeps the exported proofs and the evidence of each check, but not the compiled build directories. [My submissions](/me) shows the state of the batch and of each result: received, queued, building, judging, then accepted; awaiting review; refused, with the stage and the reason; over a limit; error, which is retried on a fresh machine; superseded, when a result received before yours was listed while yours was being checked, and yours no longer improves on it; or declined, with the reason. ## Papers {#papers} You can include a write-up of the results: put it in a folder `paper/` at the root of the submitted commit, as PDF and TeX with their sources. The preview shows which files will be included (**Paper: main.pdf, main.tex (+2 files)**). Under the permission every batch gives ([Source retention](#source-retention)), the site copies them when it archives the source and shows them on your batch's page. Once a result is listed, they can be downloaded from each listed result's page and from the [literature index](#literature). A paper is optional and lists nothing by itself. Its files never make a submission invalid, but if GitHub cannot list `paper/` again when you submit, try again in a minute. - Files go directly in `paper/` or one folder below it (`paper/figures/`). Each part of a path is a name of letters, digits and `. _ + -` that does not start with a dot, and each file has one of the extensions `.pdf`, `.tex`, `.bib`, `.bbl`, `.sty`, `.cls`, `.png`, `.jpg`, `.jpeg`, `.txt`, `.md`. - There may be at most 40 files, each PDF at most 25 MiB and each other file at most 2 MiB, 40 MiB in all. If there are more, files directly in `paper/` are taken first, then PDFs, TeX and the rest. - Anything else under `paper/`, such as a Word file, an SVG, a link, a deeper folder or a file past the limits, is left out with the warning `PAPER_FILE_IGNORED`. So is a file whose archived copy is not what the preview listed or not what its extension says, such as a `.pdf` that is not a PDF. - Every file is served as a download with its media type, a text file as `text/plain; charset=utf-8`. The site never shows a file as a page, converts it or runs it. TeX and other text files also have a plain-text address for reading them directly. - The files remain their authors'. Commit only files you may share. The Almanac offers them with your permission, and its data license (CC BY 4.0) does not cover them. A preview covers the paper's files as it covers the statements, so changing `paper/` needs a new commit and a new preview. If GitHub cannot list `paper/` (`PAPER_UNREAD`), you can submit the results without the paper, or preview again later to include it. ### The literature index {#literature} [/api/literature](/api/literature) returns every listed result by id, 100 to a page; pass a page's `next_after` as `?after=` for the next one. Each entry has the statement, its scope, the announcement date and when the site received it, the credited authors with their GitHub usernames, the check level, the sources (the repository, commit and archive URLs of a Lean check, or the paper, DOI and arXiv links of a result from before the site), and the paper's files with their URLs, sizes and SHA-256 hashes, plus a `text_url` for each text file. Results from before the site have no paper files. Reading text files at their `text_url` is limited to 120 an hour per IP address, and other downloads to 500. ## Checking before you submit {#checking-locally} The preview on [the form](/lean/submit) reads the entry file exactly as the judge will: each statement's classification and every problem with its code, location and repair. To check the proofs, build the project and print the axioms of each statement: ``` lake build AlmanacSolution printf 'import AlmanacSolution\n#print axioms AlmanacSubmission.lower_three\n' > Axioms.lean lake env lean Axioms.lean ``` The output must list only `propext`, `Classical.choice` and `Quot.sound`, and for a `native_decide` proof its certificates. This checks only your local build. ## Problem codes {#errors} Every problem in the preview has a code, a location where there is one, and a repair. The codes are stable, and [templates.json](/lean/templates.json) lists them too. ### `ENTRY_FILE_MISSING` {#error-entry-file-missing} **Entry file missing.** The commit has no AlmanacSolution.lean at the repository root. Add AlmanacSolution.lean at the root of the branch (the scaffold has one), push, and read the statements again. Blocks submission. See [Files at the root](#file-layout). Check that the file is committed at the root, not in a subdirectory, and that you pushed the branch you entered. The preview shows which commit was read. ### `ENTRY_FILE_TOO_LARGE` {#error-entry-file-too-large} **Entry file too large.** The entry file is larger than 256 KiB. Keep only imports and statements in AlmanacSolution.lean, and move proofs into imported modules. Blocks submission. See [The entry file](#entry-file). ### `ENTRY_FILE_ENCODING` {#error-entry-file-encoding} **Unsupported characters.** The entry file has an encoding or characters that are not allowed. Save it as UTF-8 without a byte-order mark, with LF or CRLF line endings, no control or bidirectional formatting characters, and spaces instead of tabs outside comments. Blocks submission. See [The entry file](#entry-file). ### `TOKEN_INVALID` {#error-token-invalid} **Unreadable token.** The entry file has an unterminated comment or «escaped» name, or a comment that begins /-/-. Close the comment or name, or add a space after /-, at the location shown. Blocks submission. See [The entry file](#entry-file). ### `TOKEN_ADJACENT` {#error-token-adjacent} **Token needs a space before it.** A comment, a «» part, or a name or number ending in a command word directly follows another token, where imported notation could change how Lean reads it. Put a space or a line break before it. Keep AlmanacSolution.lean in plain Lean syntax: if your imports change how it parses, the build is refused. Blocks submission. See [The entry file](#entry-file). For example, in Mathlib's norm `‖l.append m‖` the name `l.append`, which ends in the command word `end`, comes directly after `‖`. Write `‖ l.append m‖`. ### `LITERAL_UNSUPPORTED` {#error-literal-unsupported} **Literal not supported.** The entry file has a string, character or name literal, or a quotation. State a type that needs a literal as a definition in an imported module, and use that definition in the statement's type. Blocks submission. See [Custom statements](#custom-statements). For example, `def MyResults.Named : Prop := …` in one of your modules, with `MyResults.Named` as the statement's type. ### `LAYOUT_FILE_MISSING` {#error-layout-file-missing} **Project file missing.** A required root project file is missing. Add lean-toolchain and lakefile.toml at the repository root, and lake-manifest.json when the project has dependencies, as in the scaffold. Blocks submission. See [Files at the root](#file-layout). ### `LAKEFILE_UNSUPPORTED` {#error-lakefile-unsupported} **Unsupported lakefile.** The root lakefile.toml does not follow the Almanac's project rules. Declare the four reserved libraries and only supported settings, as in the scaffold's lakefile.toml. Blocks submission. See [Files at the root](#file-layout). ### `TOOLCHAIN_UNSUPPORTED` {#error-toolchain-unsupported} **Unsupported Lean version.** The repository's lean-toolchain is not the Lean version new submissions require. Set lean-toolchain to the version given in the directions, and rebuild. Blocks submission. See [Files at the root](#file-layout). ### `MATHLIB_UNSUPPORTED` {#error-mathlib-unsupported} **Unsupported Mathlib.** The repository's Mathlib is not pinned to the commit new submissions require. Pin Mathlib in lakefile.toml and lake-manifest.json to the commit given in the directions. Blocks submission. See [Files at the root](#file-layout). ### `MATHLIB_PACKAGE_MISMATCH` {#error-mathlib-package-mismatch} **Mathlib package mismatch.** A Mathlib package's address or commit doesn't match the judge's copy, so the build would fail. Fix it in both lake-manifest.json and lakefile.toml, then read the statements again. Blocks submission. See [Files at the root](#file-layout). ### `HEADER_UNSUPPORTED` {#error-header-unsupported} **Unsupported text before the namespace.** Something other than comments and plain import lines comes before namespace AlmanacSubmission. Keep only comments and lines such as `import ExampleProject.Results` before the namespace; move options, `open` commands and declarations into an imported module. Blocks submission. See [The entry file](#entry-file). `open`, `set_option` and `variable` before the namespace would change how the rest of the file is read. Write full names instead. ### `NAMESPACE_MISSING` {#error-namespace-missing} **Namespace missing.** The entry file has no namespace AlmanacSubmission block. Put the statements between `namespace AlmanacSubmission` and `end AlmanacSubmission`. Blocks submission. See [The entry file](#entry-file). ### `NAMESPACE_UNTERMINATED` {#error-namespace-unterminated} **Namespace not closed.** namespace AlmanacSubmission is not closed by end AlmanacSubmission. End the block with `end AlmanacSubmission`, written on one line. Blocks submission. See [The entry file](#entry-file). ### `WRAPPER_SYNTAX_UNSUPPORTED` {#error-wrapper-syntax-unsupported} **Unsupported declaration.** The namespace contains something other than theorems of the supported form. Write each result as `theorem lower_example : Almanac.LowerBoundAt 3 9 := ExampleProject.lower_example`, and move definitions, options, attributes and commands into an imported module. Blocks submission. See [The entry file](#entry-file). ### `BINDERS_UNSUPPORTED` {#error-binders-unsupported} **Binders before the colon.** A theorem in the namespace has binders between its name and its colon. Move them into the type after the colon, as `∀ (n : Nat), …` or an implication; such a statement is custom. Blocks submission. See [Custom statements](#custom-statements). `theorem w (n : Nat) : P n := …` becomes `theorem w : ∀ n : Nat, P n := …`, a custom statement. A template never has binders. ### `THEOREM_TYPE_REQUIRED` {#error-theorem-type-required} **Type required.** A theorem in the namespace has no type after its name. Write the template type, as in `theorem lower_example : Almanac.LowerBoundAt 3 9 := ExampleProject.lower_example`, or the inferred form `theorem name : type_of% Fully.Qualified.theorem := Fully.Qualified.theorem`, which is a custom statement. Blocks submission. See [The entry file](#entry-file). ### `PROOF_REFERENCE_UNSUPPORTED` {#error-proof-reference-unsupported} **Unsupported proof.** A statement's proof is not one fully qualified theorem name, written `Name` or `by exact Name`. Prove the result in an imported module and write `:= Fully.Qualified.theorem`. If the theorem needs arguments or a bridge, prove a linking lemma there and use that. Blocks submission. See [Linking lemmas](#linking-lemmas). Tactic blocks, applications such as `Foo.bar 3`, and `(Foo.bar)` are all refused. ### `IDENTIFIER_INVALID` {#error-identifier-invalid} **Invalid statement name.** A statement's name is not a simple ASCII identifier of at most 64 characters. Use letters, digits and underscores, starting with a letter or underscore, with no dots, «» or Lean keywords. Blocks submission. See [The entry file](#entry-file). ### `DUPLICATE_THEOREM_NAME` {#error-duplicate-theorem-name} **Duplicate statement name.** Two statements have the same name. Rename one of them. Blocks submission. See [The entry file](#entry-file). ### `NO_SUBMITTED_THEOREMS` {#error-no-submitted-theorems} **No statements.** namespace AlmanacSubmission contains no statements. Add one theorem for each result, such as `theorem lower_example : Almanac.LowerBoundAt 3 9 := ExampleProject.lower_example`. Blocks submission. See [The entry file](#entry-file). ### `BATCH_LIMIT_EXCEEDED` {#error-batch-limit-exceeded} **Too many statements.** The entry file has more than 24 statements. Submit at most 24 results in one batch, and the rest in a later one. Blocks submission. See [The entry file](#entry-file). ### `TEMPLATE_NAME_UNQUALIFIED` {#error-template-name-unqualified} **Template name not qualified.** A statement's type uses a template name without the Almanac. prefix. Write the full name, such as `Almanac.LowerBoundAt`; templates are never found through `open`. Blocks submission. See [Templates](#templates). ### `TEMPLATE_PARAMETER_INVALID` {#error-template-parameter-invalid} **Invalid template parameter.** A template parameter is not a value the template accepts. Write it as in the template's table: a natural literal in range, a reduced fraction, or an `Almanac.Expr` constructor term. Blocks submission. See [Templates](#templates). ### `TEMPLATE_PARAMETER_NONCANONICAL` {#error-template-parameter-noncanonical} **Parameter not in canonical form.** A template parameter is not written in canonical form. Replace the type with the canonical text shown. Blocks submission. See [Templates](#templates). Lean elaborates `2/6` and `1/3` differently, so only the canonical text can match the trusted statement. ### `TEMPLATE_WORK_EXCEEDED` {#error-template-work-exceeded} **Templates too large to read.** The file's template parameters are too large to read in one preview. Simplify the formulas, or submit some of the results in a later batch. Blocks submission. See [Templates](#templates). ### `TEMPLATE_HEAD_NOT_EXACT` {#error-template-head-not-exact} **Template not used exactly.** The type uses an Almanac template, but not as the whole statement with exactly its parameters, so it is a custom statement. For automatic recognition, make the type exactly the template applied to its parameters, and move hypotheses or conjunctions into linking lemmas or separate statements. Warning only; does not block submission. See [Custom statements](#custom-statements). A coefficient written `7/2` without parentheses is three arguments; write `(7/2)`. ### `TEMPLATE_SCALE_UNSUPPORTED` {#error-template-scale-unsupported} **Unsupported factorial scale.** The factorial-scale template uses a k other than 3 or 4, so it is a custom statement. Use k = 3 or k = 4 for automatic recognition; other scales need manual interpretation. Warning only; does not block submission. See [Templates](#templates). ### `CUSTOM_EXPLICIT_TYPE` {#error-custom-explicit-type} **Custom statement.** The statement's type is not a supported template, so it needs manual interpretation. If it is equivalent to a supported template, prove that template in an imported linking lemma and point the statement at it. Warning only; does not block submission. See [Custom statements](#custom-statements). ### `CUSTOM_INFERRED_TYPE` {#error-custom-inferred-type} **Inferred type.** The statement's type is inferred from its proof, so it is a custom statement even if the type matches a template. Write the template type after the colon for automatic recognition. Warning only; does not block submission. See [Custom statements](#custom-statements). `type_of% Foo.bar` stays custom even when the type of `Foo.bar` is a template. ### `DUPLICATE_STATEMENT` {#error-duplicate-statement} **Duplicate statement.** Two statements in the batch state the same claim. Keep one of them. Information only; does not block submission. See [The entry file](#entry-file). ### `NO_IMPROVEMENT` {#error-no-improvement} **No improvement.** The claim does not improve a currently accepted public result. Remove the statement or strengthen it: a result that adds nothing is not listed. Blocks submission. See [Reading the preview](#preview). The message shows the public result that already gives each value. Ties are not listed. ### `KERNEL_UPGRADE_POSSIBLE` {#error-kernel-upgrade-possible} **Possible kernel upgrade.** The claim may improve the kernel-checked track, where the current result is native-checked. Nothing to do: which track it joins depends on how its proof is checked. Information only; does not block submission. See [Reading the preview](#preview). ### `UNSCORED_TARGET` {#error-unscored-target} **No points prize.** The claim concerns a supported target that has no points prize. Nothing to do: it can still improve the listed bounds. Information only; does not block submission. See [Reading the preview](#preview). ### `CLAIM_INCONSISTENT` {#error-claim-inconsistent} **Inconsistent claims.** The claim contradicts another claim in the batch or an accepted public result. Check both statements' directions and parameters; the batch cannot be submitted with both. Blocks submission. See [Reading the preview](#preview). Neither claim gets an estimate. ### `CLAIM_IMPOSSIBLE` {#error-claim-impossible} **Impossible claim.** The claim contradicts a bound that holds for every n, so no proof of it can exist. Check the statement's direction and parameters. Blocks submission. See [Templates](#templates). ### `REPOSITORY_NOT_FOUND` {#error-repository-not-found} **Repository not found.** The repository does not exist on GitHub or is not public. Check the repository's name, and make it public. Blocks submission. See [Reading the preview](#preview). ### `REF_NOT_FOUND` {#error-ref-not-found} **Branch, tag or commit not found.** The branch, tag or commit does not exist in the repository. Check the name, or leave it blank for the default branch. Blocks submission. See [Reading the preview](#preview). ### `GITHUB_UNAVAILABLE` {#error-github-unavailable} **GitHub unavailable.** GitHub did not answer the request. Try again in a minute; nothing is wrong with the source. Blocks submission. Trying again can clear it. See [Reading the preview](#preview). ### `GITHUB_RATE_LIMITED` {#error-github-rate-limited} **GitHub rate limit.** GitHub's request limit was reached. Nothing is wrong with the source: read the statements again after the time shown. Blocks submission. Trying again can clear it. See [Reading the preview](#preview). Everyone who previews shares the site's allowance of GitHub requests (the site may use a read-only token of its own). ### `PREVIEW_RATE_LIMITED` {#error-preview-rate-limited} **Too many previews.** Too many previews were requested in a short time. Wait a minute, then read the statements again. Blocks submission. Trying again can clear it. See [Reading the preview](#preview). ### `PREVIEW_EXPIRED` {#error-preview-expired} **Preview expired.** The preview is more than 15 minutes old. Read the statements again, then submit. Blocks submission. Trying again can clear it. See [Reading the preview](#preview). ### `PREVIEW_INVALID` {#error-preview-invalid} **Preview not valid.** The preview token is not one the site issued for this account and source. Read the statements again, then submit. Blocks submission. Trying again can clear it. See [Reading the preview](#preview). ### `SOURCE_CHANGED` {#error-source-changed} **Source changed.** The entry file or its statements differ from the previewed ones. Read the statements again and check them before submitting. Blocks submission. Trying again can clear it. See [Reading the preview](#preview). You won't see this just because the branch moved after the preview: the previewed commit is the one submitted. ### `SIGN_IN_REQUIRED` {#error-sign-in-required} **Sign in required.** Previews and submissions need a signed-in account. Sign in with GitHub. Blocks submission. See [Quick start](#quick-start). ### `ACCOUNT_LIMIT` {#error-account-limit} **Submission limit reached.** You have sent as many submissions as allowed in 24 hours. Submit again once the earliest of them is 24 hours old. Blocks submission. See [Quick start](#quick-start). ### `SUBMISSIONS_CLOSED` {#error-submissions-closed} **Submissions closed.** Lean submissions are not open. Try again when the directions say submissions are open. Blocks submission. See [Quick start](#quick-start). ### `REPOSITORY_INVALID` {#error-repository-invalid} **Not a GitHub repository address.** The repository is not given as https://github.com/OWNER/REPO. Give the repository's address on github.com, such as https://github.com/OWNER/REPO. Blocks submission. See [Reading the preview](#preview). ### `REF_INVALID` {#error-ref-invalid} **Branch, tag or commit not valid.** This is not a valid branch or tag name or a full commit SHA, or it is both a branch and a tag. Give a branch or tag name, or the full 40-character commit SHA; leave it blank for the default branch. Blocks submission. See [Reading the preview](#preview). Branch and tag names may use letters, digits and `. _ / + @ -`. For anything else, give the full 40-character commit SHA. ### `MANIFEST_UNSUPPORTED` {#error-manifest-unsupported} **Unsupported lake-manifest.json.** The root lake-manifest.json does not follow the Almanac's dependency rules. List each dependency as a git repository on github.com pinned to a full commit SHA, as Lake writes it. Blocks submission. See [Files at the root](#file-layout). ### `CHECKER_UNAVAILABLE` {#error-checker-unavailable} **Checker unavailable.** The checker for the Lean version new submissions require is not available right now. Try again later; nothing is wrong with the source. Blocks submission. Trying again can clear it. See [Quick start](#quick-start). ### `PREVIEW_OUTDATED` {#error-preview-outdated} **Preview outdated.** The required Lean version, or the site's parser or templates, changed after the preview. Read the statements again, then submit. Blocks submission. Trying again can clear it. See [Reading the preview](#preview). ### `ACCOUNT_BUSY` {#error-account-busy} **Submission still being checked.** You have a submission that is still being checked. Read the statements again once it has finished. Blocks submission. See [Quick start](#quick-start). ### `ACCOUNT_RESTRICTED` {#error-account-restricted} **Account restricted.** This account cannot submit proofs. This cannot be changed from the repository or this form. Blocks submission. See [Quick start](#quick-start). ### `REQUEST_INVALID` {#error-request-invalid} **Request not accepted.** The request did not come from the site's form with a valid security token. Reload the submission page, then read the statements again. Blocks submission. See [Reading the preview](#preview). ### `PAPER_FILE_IGNORED` {#error-paper-file-ignored} **Paper file ignored.** A file under paper/ is not one the site archives with the results. Keep paper/ to at most 40 PDF, TeX, bibliography, style, Markdown, text, PNG and JPEG files, directly in it or one folder below, with plain names; the results can be submitted either way. Warning only; does not block submission. See [Papers](#papers). The warning lists the first files left out and why. The other files in `paper/` are still taken, and the results do not depend on any of them. ### `PAPER_UNREAD` {#error-paper-unread} **Paper not read.** The files under paper/ could not be listed. Read the statements again later to include the paper; the results can be submitted without it. Warning only; does not block submission. Trying again can clear it. See [Papers](#papers). ### `REPOSITORY_NOT_OWNED` {#error-repository-not-owned} **Not your repository.** The repository is not under the GitHub account you signed in with. Submit from a public repository under your own GitHub account. To submit someone else's proof, ask them to submit it. Blocks submission. See [Quick start](#quick-start). ### `REPOSITORY_ORGANIZATION` {#error-repository-organization} **Organization repository.** The repository belongs to an organization. Organization repositories aren't supported yet. Push the branch to a public repository under your own GitHub account, and submit that. Blocks submission. See [Quick start](#quick-start). ### `REPOSITORY_FORK` {#error-repository-fork} **Forked repository.** The repository is a fork. Create a new repository under your own GitHub account, not a fork, and push the branch to it. Blocks submission. See [Quick start](#quick-start). ### `COMMIT_NOT_ON_BRANCH` {#error-commit-not-on-branch} **Commit not on a branch or tag.** The commit was not found on the repository's branches and tags. Give a branch or tag of this repository that has the commit. If none does, tag the commit or push it to a branch. Blocks submission. See [Reading the preview](#preview). ### `HOSTING_PERMISSION_REQUIRED` {#error-hosting-permission-required} **Permission not given.** The permission to keep and host the commit's files was not given. Tick the permission box above the submit button, then submit again. Blocks submission. See [Source retention](#source-retention). ## Updating results {#updating-results} A later submission lists only new or stronger results. Accepted results keep their evidence, date, credit and check level, whether or not the new file still has their statements, and they are not checked again. To improve a result, submit the stronger claim. To upgrade a `native_decide` result to kernel-checked, submit a kernel-checked proof of the same statement; it is a new result, dated when it is received. Never edit a submitted commit: submit a new one. ## Lean version {#lean-version} New submissions must use the latest stable Lean release and, if they use Mathlib, the exact commit listed on this page. Release candidates are not accepted. The site checks Lean's official release information for each preview and each submission, and reuses a successful check for at most five minutes. If a newer stable release is not yet supported, or the site cannot confirm the current release, new submissions pause. Proofs already received are completed and rechecked in their recorded environment. Older environments are kept for historical results but cannot be chosen for new submissions. A version retired for a soundness problem cannot be used. ## Limits {#limits} | Stage | Limit | Machine | |---|---|---| | Fetch | 15 minutes | build machine | | Build and export | 2 hours, memory 30 GiB | 8 CPUs, 32 GB | | `native_decide` re-evaluation | 2 hours | build machine | | Judge: compare, axioms, both replays | 12 hours, memory 14 GiB | 4 CPUs, 16 GB | | Repository and dependencies | 500 MiB at the commit | | | Each Lean file of yours | 10,000 lines | | | Export of the proof | 4 GiB | | A batch is one job, so these limits are for the whole batch, not for each result. A job that exceeds a limit stops as "over a limit" and is reviewed with its measurements. It may be given a run with fewer CPUs (Lake runs one `lean` per CPU, so fewer CPUs need less memory) or one run on a bigger machine, or be declined with a reason that you will see. The build machine compiles files in parallel on its 8 CPUs, but only files that do not import one another. A large proof split into several independent files, all imported by `AlmanacSolution.lean`, builds faster than one large file. The judge's two kernel checks run at the same time, each on one CPU whatever the layout, so their time depends on how much the kernel must compute. Large `decide` proofs are the usual cause of a slow check. ## The definitions file {#definitions} `AlmanacDefs.lean` defines superpermutations, formulas and the templates. It uses only Lean's core, so it is the same for every allowed version: [download it](/lean/AlmanacDefs.lean). ```lean /-! # Superpermutation Almanac: the definitions file Published by the Almanac, the same for every submission at a given Lean version. It imports nothing beyond Lean's core, so it compiles unchanged on every allowed toolchain. The judge writes this file over any file of the same name in a submitted repository. -/ namespace Almanac /-- A word on `n` symbols. -/ abbrev Word (n : Nat) : Type := List (Fin n) /-- `w` is a superpermutation on `n` symbols: every arrangement of the `n` symbols (a duplicate-free word of length `n`) occurs in `w` as a contiguous block. -/ def IsSuperpermutation (n : Nat) (w : Word n) : Prop := ∀ p : Word n, p.Nodup → p.length = n → p <:+: w /-- The factorial, defined here because core Lean has none. -/ def fact : Nat → Nat | 0 => 1 | k + 1 => (k + 1) * fact k /-- A formula in `n`, evaluated in `Rat`: rational constants, `n`, `+`, `-`, `*`, powers `n ^ j`, factorials `(n - k)!`, and division. The site checks that every divisor is positive and every `k` is at most `n₀` before it writes a statement. -/ inductive Expr where | const (q : Rat) | var | add (a b : Expr) | sub (a b : Expr) | mul (a b : Expr) | pow (j : Nat) | fact (k : Nat) | div (a b : Expr) /-- The value of a formula at `n`. -/ def Expr.eval (n : Nat) : Expr → Rat | .const q => q | .var => (n : Rat) | .add a b => a.eval n + b.eval n | .sub a b => a.eval n - b.eval n | .mul a b => a.eval n * b.eval n | .pow j => (n : Rat) ^ j | .fact k => ((Almanac.fact (n - k) : Nat) : Rat) | .div a b => a.eval n / b.eval n /-- Shape 1: every superpermutation on `n` symbols has length at least `v`. -/ def LowerBoundAt (n v : Nat) : Prop := ∀ w : Word n, IsSuperpermutation n w → v ≤ w.length /-- Shape 2: for every `n ≥ n₀`, every superpermutation on `n` symbols has length at least `f n`. -/ def LowerBoundFrom (n₀ : Nat) (f : Expr) : Prop := ∀ n : Nat, n₀ ≤ n → ∀ w : Word n, IsSuperpermutation n w → f.eval n ≤ (w.length : Rat) /-- Shape 2: for `n₀ ≤ n ≤ n₁`, every superpermutation on `n` symbols has length at least `f n`. -/ def LowerBoundRange (n₀ n₁ : Nat) (f : Expr) : Prop := ∀ n : Nat, n₀ ≤ n → n ≤ n₁ → ∀ w : Word n, IsSuperpermutation n w → f.eval n ≤ (w.length : Rat) /-- Shape 2: for every `n ≥ n₀` there is a superpermutation on `n` symbols of length at most `f n`. -/ def UpperBoundFrom (n₀ : Nat) (f : Expr) : Prop := ∀ n : Nat, n₀ ≤ n → ∃ w : Word n, IsSuperpermutation n w ∧ (w.length : Rat) ≤ f.eval n /-- `n! + (n-1)! + (n-2)! + c (n-3)!`, the form of the asymptotic shapes. -/ def asymptoticForm (n : Nat) (c : Rat) : Rat := (fact n : Rat) + (fact (n - 1) : Rat) + (fact (n - 2) : Rat) + c * (fact (n - 3) : Rat) /-- Shape 3: for every `ε > 0`, for all large `n`, some superpermutation on `n` symbols has length at most `n! + (n-1)! + (n-2)! + (c + ε) (n-3)!`. -/ def AsymptoticUpper (c : Rat) : Prop := ∀ ε : Rat, 0 < ε → ∃ N : Nat, ∀ n : Nat, N ≤ n → ∃ w : Word n, IsSuperpermutation n w ∧ (w.length : Rat) ≤ asymptoticForm n (c + ε) /-- Shape 3: for every `ε > 0`, for all large `n`, every superpermutation on `n` symbols has length at least `n! + (n-1)! + (n-2)! + (c - ε) (n-3)!`. -/ def AsymptoticLower (c : Rat) : Prop := ∀ ε : Rat, 0 < ε → ∃ N : Nat, ∀ n : Nat, N ≤ n → ∀ w : Word n, IsSuperpermutation n w → asymptoticForm n (c - ε) ≤ (w.length : Rat) end Almanac /-! ## Factorial-scale asymptotic shapes Added for batch submissions (Oct 27, 2026); everything above is unchanged. `asymptoticFormAt 3` is `asymptoticForm`, so `AsymptoticUpperAt 3 c` and `AsymptoticLowerAt 3 c` are `AsymptoticUpper c` and `AsymptoticLower c` by definition. -/ namespace Almanac /-- `n! + (n-1)! + (n-2)! + c (n-k)!`, the form of the factorial-scale asymptotic shapes. -/ def asymptoticFormAt (k n : Nat) (c : Rat) : Rat := (fact n : Rat) + (fact (n - 1) : Rat) + (fact (n - 2) : Rat) + c * (fact (n - k) : Rat) /-- Shape 3 at the scale `(n-k)!`: for every `ε > 0`, for all large `n`, some superpermutation on `n` symbols has length at most `n! + (n-1)! + (n-2)! + (c + ε) (n-k)!`. -/ def AsymptoticUpperAt (k : Nat) (c : Rat) : Prop := ∀ ε : Rat, 0 < ε → ∃ N : Nat, ∀ n : Nat, N ≤ n → ∃ w : Word n, IsSuperpermutation n w ∧ (w.length : Rat) ≤ asymptoticFormAt k n (c + ε) /-- Shape 3 at the scale `(n-k)!`: for every `ε > 0`, for all large `n`, every superpermutation on `n` symbols has length at least `n! + (n-1)! + (n-2)! + (c - ε) (n-k)!`. -/ def AsymptoticLowerAt (k : Nat) (c : Rat) : Prop := ∀ ε : Rat, 0 < ε → ∃ N : Nat, ∀ n : Nat, N ≤ n → ∀ w : Word n, IsSuperpermutation n w → asymptoticFormAt k n (c - ε) ≤ (w.length : Rat) end Almanac ```