/mathlib4

Work in progress mathlib port for lean 4

Primary LanguageLeanApache License 2.0Apache-2.0

mathlib4

Work in progress mathlib port for Lean 4. This is not a port. We are just trying things out to gain experience for the real port.

We're not planning to have any review standards in the mathlib4 repo higher than your average wiki during this experimentation phase.

We don't want to discourage others from trying to port stuff if it helps us learn how to work in lean 4, but please understand that anything that is currently in mathlib4 is subject to change/deletion, and the "real" port hasn't started yet