Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?]

Marko Rauhamaa marko at
Sat Aug 8 23:27:00 CEST 2015

Marko Rauhamaa <marko at>:

> Steven D'Aprano <steve+comp.lang.python at>:
>> The contemporary standard approach is from Zermelo-Fraenkel set
>> theory: define 0 as the empty set, and the successor to n as the
>> union of n and the set containing n:
>> 0 = {} (the empty set) 
>> n + 1 = n ∪ {n}
> That definition barely captures the essence of what a number *is*. In
> fact, there have been different formulations of natural numbers.

Rehashing this old discussion. I ran into this wonderful website:


It is an absolute treasure for those of us who hate handwaving in math
textbooks. The database of computer-checked theorems proves everything
starting from the very bottom.

An interesting, recurring dividing line among the proofs is a layer of
"provable" axioms. For example, this proof

(for "⊢ (2 + 2) = 4") references the axiom (<URL:>):

   ⊢ 1 ∈ ℂ

The axiom is "justified by" a set-theoretic theorem:

   Description: 1 is a complex number. Axiom 2 of 22 for real and
   complex numbers, derived from ZF set theory. This
   construction-dependent theorem should not be referenced directly;
   instead, use ax-1cn 7963.

In other words, since there is no canonical way to define numbers in set
theory, Metamath insulates its proofs from a particular definition by
circumscribing numbers with construction-independent axioms.

Anyway, ob. Python reference:

   Using the design ideas implemented in Metamath, Raph Levien has
   implemented what might be the smallest proof checker in the world,, at only 500 lines of Python code.


More information about the Python-list mailing list