This paper reconstructs the Peircean interpretation of Kant's doctrine on the syntheticity of mathematics. Peirce correctly locates Kant's distinction in two different sources: Kant's lack of access to polyadic logic and, more interestingly, Kant's insight into the role of ingenious experiments required in theorem-proving. In this second respect, Kant's analytic/synthetic distinction is identical with the distinction Peirce discovered among types of mathematical reasoning. I contrast this Peircean theory with two other prominent views on Kant's syntheticity, i.e. the Russellian and the Beckian views, and show how Peirce's interpretation of Kant solves the dilemma that each of these two views faces. I also show that Hintikka's criterion for Kant's synthetic judgments, i.e. a new individual introduced by the ∃-instantiation rule, does not capture the most important characteristic of Peirce's theorematic reasoning, i.e. the process of choosing a correct individual.