← All papers
First page of From Swap Axioms to Weighted Geometric Means: A Characterization of AMMs

From Swap Axioms to Weighted Geometric Means: A Characterization of AMMs

Björn Assmann, Ulan Degenbaev

cs.DC Apr 18, 2026 · v1
A machine-checked Lean 4 formalization accompanies the AMM characterization proofs.
Many automated market makers can be understood through the geometry of their trading orbits, the sets of states reachable from one another through swaps. In prominent designs, this geometry is captured by a simple closed-form invariant such as the constant product $xy$ in Uniswap or a weighted geometric mean $x^w y^{1-w}$ in Balancer. This paper explains why these forms arise by deriving them from three basic assumptions: validity invariance (swaps preserve the validity of states), Pareto efficiency (no state on an orbit weakly dominates another), and unit invariance (changing measurement units does not change the mechanism). Together, these force every trading orbit of a two-asset AMM to be a level set of a weighted geometric mean $x^w y^{1-w}$. Applied pairwise, the axioms extend the classification to $n$-asset pools: orbits are level sets of $\prod_i x_i^{w_i}$ with positive weights $w_i$ summing to $1$. Imposing token-relabeling symmetry then pins down the weights, recovering the constant-product form $xy$ in the two-asset case and $\prod_i x_i$ in general. The main text provides an intuitive proof sketch and discusses fees and liquidity operations. Complete proofs and a machine-checked Lean 4 formalization accompany the paper.

Automated market makers like Uniswap and Balancer use specific invariant functions (constant product, weighted geometric mean), but there was no derivation of these forms from simple first-principles axioms on the swap rule itself.

The paper derives the invariant curve from three basic assumptions: validity invariance (swaps preserve valid states), Pareto efficiency (no state on an orbit weakly dominates another), and unit invariance (changing measurement units does not change the mechanism). The authors show these force every two-asset AMM trading orbit to be a level set of a weighted geometric mean x^w y^{1-w}. A machine-checked Lean 4 formalization accompanies the paper.

The three axioms uniquely characterize weighted geometric mean invariants for two-asset AMMs, extending to n-asset pools as products with positive weights summing to 1. Imposing token-relabeling symmetry recovers the constant-product form. Complete proofs and a Lean 4 formalization are provided.