## Stream: new members

### Topic: Proving properties about floating point arithmetic

#### Huỳnh Trần Khanh (Jan 04 2021 at 07:41):

Can I prove that something like this is correct in Lean 4? Or is Lean 4 not capable enough?

#### Huỳnh Trần Khanh (Jan 04 2021 at 07:50):

Apologies if I sound stupid, I am pretty much a noob.

#### Eric Wieser (Jan 04 2021 at 07:59):

I'm sure you could do it in lean 3 too, but in both cases you'll have to start by telling lean the rules of floating point numbers

#### Eric Wieser (Jan 04 2021 at 08:00):

Mathlib has a start at that in docs#fp.float

#### Yakov Pechersky (Jan 04 2021 at 08:01):

There are also docs#unsigned integers, but I haven't seen anything about how conversion of the bit patterns from unsigned to signed is the modulo operation (for some fixed bit width, here I think you use 64)

#### Yakov Pechersky (Jan 04 2021 at 08:02):

The definition at https://github.com/kth-competitive-programming/kactl/blob/master/doc/modmul-proof.md has an M and a c, and I can't tell which is the typo

#### Eric Wieser (Jan 04 2021 at 08:04):

A better link than @Huỳnh Trần Khanh's: non-raw github

#### Eric Wieser (Jan 04 2021 at 08:06):

Note that the proof @Yakov Pechersky links to starts with a false assumption about the precision of long double, which is platform-dependent, most notably equal to double on windows

#### Huỳnh Trần Khanh (Jan 04 2021 at 08:12):

I'd assume M is the typo because the rest of the proof uses c. Maybe I should file an issue against the repo.