diff --git a/formalization.yaml b/formalization.yaml
new file mode 100644
index 0000000..1627d74
--- /dev/null
+++ b/formalization.yaml
@@ -0,0 +1,69 @@
+# yaml-language-server: $schema=https://raw.githubusercontent.com/mathlib-initiative/formalization.yaml/main/schema/formalization.schema.json
+
+version: "v0.4"
+
+project:
+  name: "PartitionElliptic"
+  authors: [Kenny Lau]
+  description: >
+    `PartitionElliptic` is a formal proof of the two identities of *Two Key Identities for Formal
+    Verification*, the spec accompanying Ken Ono's *The partition function and elliptic curves*.
+    It proves Key Formula 1 and Key Formula 2. The Lean files were generated by AxiomProver,
+    Axiom Math's in-house theorem proving system.
+  responsible_maintainers: [Kenny Lau]
+  license: "MIT"
+
+repository:
+  role: "substantive-development"
+
+sources:
+  - title: "Two Key Identities for Formal Verification"
+    type: "article"
+    location: "Key Formula 1, Key Formula 2"
+    relationship: "formalizes"
+    note: >
+      The spec singles these two identities out of its companion paper, Ken Ono's *The partition
+      function and elliptic curves*, for formal verification.
+
+status:
+  scope: >
+    Key Formula 1 and Key Formula 2, as identities between complex numbers. `problem.lean` takes
+    the values of the modular objects at a fixed $\tau$ as given data subject to $E_4 \ne 0$,
+    $J \ne 1728$ and $\Phi_Y \ne 0$, exactly as the spec's ground data does.
+  sorry_count: 0
+  sorry_in_definitions: 0
+  axioms: [propext, Quot.sound, Classical.choice]
+  main_results:
+  - declaration: "key_formula_one"
+    file: "output/solution.lean"
+    sorry_count: 0
+    axioms: [propext, Quot.sound, Classical.choice]
+    comparator_config: "comparator.json"
+  - declaration: "key_formula_two"
+    file: "output/solution.lean"
+    sorry_count: 0
+    axioms: [propext, Quot.sound, Classical.choice]
+    comparator_config: "comparator.json"
+
+automation:
+  methods:
+    - method: "autonomous"
+      models: [AxiomProver]
+
+review:
+  status: "author-verified"
+  reviewers: [Kenny Lau]
+  notes: >
+    The formal challenge in `output/problem.lean` was checked against the source paper by an
+    author of that paper.
+
+alignment:
+  statements:
+    - source: "Two Key Identities for Formal Verification (Key Formula 1)"
+      lean: "key_formula_one"
+      module: "output.solution"
+      status: "Proved."
+    - source: "Two Key Identities for Formal Verification (Key Formula 2)"
+      lean: "key_formula_two"
+      module: "output.solution"
+      status: "Proved."