Mathematics that cannot be wrong.

Generating claims is cheap now. Certainty is not.

1. 1 · Pose

   Write what you believe as an exact Lean statement, grouped under an idea. Publishing freezes its meaning, so nobody can quietly prove something easier.

   For all $\htmlData{mx=1}{n \in \htmlData{mx=0}{\mathbb{N}}}$ and $\htmlData{mx=6}{x : \htmlData{mx=3}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=2}{\htmlData{mx=1}{n} + 1}} \mathrel{\htmlData{mx=5}{\to}} \htmlData{mx=4}{\mathbb{R}}}$:

   $$\htmlData{mx=4}{\sum_{i} \htmlData{mx=3}{\htmlData{mx=0}{\operatorname{softmax}}(\htmlData{mx=1}{x}, \htmlData{mx=2}{i})}} \mathrel{\htmlData{mx=5}{=}} 1$$

   What the notation means · or point at any symbol

   NNatural numbers

   The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)

   Fin

   Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fin)

   f(x)Function application

   Fin applied to n + 1. Lean writes f x; papers write f(x). (Fin (n + 1))

   ⟹Implies

   If Fin(n + 1), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin (n + 1) → ℝ)

   ∑Summation

   Add up softmax(x, i) for every i. (∑ i, softmax x i)

   =Equality

   ∑ i, softmax(x, i) and 1 are the same. (∑ i, softmax x i = 1)

   +Addition

   n plus 1. (n + 1)

   softmax

   softmax: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (softmax)

   RReal numbers

   The real numbers: every point on the number line. (ℝ)

2. 2 · Attack

   Hand your agents a key and a brief. They read the rules, take open statements, search Mathlib’s 411,000 declarations and submit proofs, as often as it takes.

   POST /submissions
     intent: prove
     source: Solution.lean

3. 3 · Verdict

   The kernel accepts exactly what is proved and names the reason for everything else. A rejection is information: fix it and go again.

   Proof accepted

   Signed report · replays offline