Math formalization: Puiseux, Banach–Tarski, π-free trig

Stream: new members

[Daniel de Rauglaudre]

Hello everyone,

I’m a retired research engineer (ex-Inria, Coq/Rocq community), and
I’ve been formalizing mathematics in Coq for many years.

Some projects I’ve completed in Rocq:

• a formal proof of Puiseux’s theorem (~30k lines),
• Banach–Tarski (~10k lines, plus an article), and
• a “π-free trigonometry” where angles are pairs (x,y) with x²+y²=1.

I’m interested in exchanging ideas with people working on unusual or
foundational aspects of formalized mathematics. Not here to learn
Lean, but curious to share and discuss with the Lean/Mathlib
community.

Cheers,

Daniel de Rauglaudre

[Yan Yablonovskiy 🇺🇦]

Welcome! :smiley:

You may be interested in:
https://github.com/Bergschaf/lean-banach-tarski

[Daniel de Rauglaudre]

Hi Yan,

Thanks for the pointer! I’m aware of other Banach–Tarski formalizations, but my work in Rocq/Coq is quite different. I’m exploring “ring-like” algebra (a unifying framework covering semirings, rings, and fields, with optional operations like subtraction or inverses), trig without π, and other constructions—more focused on frameworks and methods than reproducing known results.

Cheers,

Daniel

[Yan Yablonovskiy 🇺🇦]

Interesting, well depending what you mean by ring-like, i am working on some formalisations of Algebraic Wheels in https://github.com/YanYablonovskiy/AlgebraicWheelTheory , these contain certain semi-rings and are kind of like generalisations.

I hesitated to reply in thread, figured will wait for others to be more helpful(its a timezone thing, this time is less active)

[Daniel de Rauglaudre]

Let me explain briefly what I mean by ring-like.

In my framework, instead of defining separately semirings, rings,
ordered rings, fields, etc., I use a single structure with boolean
flags to indicate which extra operations or axioms are available.

For example:
– has_opp says whether additive inverses exist (so a semiring with
has_opp = false, a ring with has_opp = true).
– mul_is_comm tells whether multiplication is commutative.
– is_ordered says whether there is a compatible order.
– has_subt for primitive subtraction, etc.

This way, I can state many theorems in a more general setting, without
having to duplicate them for each algebraic structure.

In this framework, axioms themselves can be conditional.
For instance:
– mul_assoc is unconditional:
∀ a b c, a * (b * c) = (a * b) * c.
– mul_comm is conditional: it has type
if mul_is_comm then ∀ a b, a * b = b * a else not_applicable.

This makes it possible to capture in one unified system both
commutative and non-commutative structures, ordered and unordered
ones, etc., without duplicating the whole theory.

My whole library is here: https://roglo.github.io/rocq_ring_like/

[Eric Wieser]

I think Lean uses the extends keyword to avoid this duplication, for instance see src#CommRing

[Eric Wieser]

The advantage of this approach is that you don't have to commit to every axiom that could exist up front

[Eric Wieser]

(eg, if you want to talk about rings that are alternative but not associative like the octonions)

[Junyan Xu]

The slowdowns at #28604 and #28532 makes me think whether we should unbundle associativity and commutativity; unbundling one and neg may be harder. Interestingly I was able to control the slowdown from NonAssocCommSemiring down to 0.05/0.12% by using priority 10 instances, but once I added NonAssocCommRing it jumps to 0.35/0.245% again.