diff options
| author | Anthony Wang | 2025-05-06 00:59:39 -0400 |
|---|---|---|
| committer | Anthony Wang | 2025-05-06 00:59:39 -0400 |
| commit | 305480cfca80c51a26fa644be78dab6eedf52e9e (patch) | |
| tree | 48674ab4c64ae376de07a85aa4a59200aaf2abd9 | |
| parent | b4b11797e9b29c5ddacaf9897b5154c75e533c06 (diff) | |
Rewrite it in Lean
| -rw-r--r-- | src/denom.lean | 12 | ||||
| -rw-r--r-- | src/denom.py | 4 |
2 files changed, 12 insertions, 4 deletions
diff --git a/src/denom.lean b/src/denom.lean new file mode 100644 index 0000000..93e2692 --- /dev/null +++ b/src/denom.lean @@ -0,0 +1,12 @@ +# x = 1 - 0.9772532922866427 +# for i in range(1, 10000): +# if abs(x * i - round(x * i)) < 1e-4: +# print(i, x * i) + +def x := 1 - 0.9772532922866427 + +def N := 10000 + +def A := (List.range N).map λ a => a + 1 + +#eval A.filter λ a => Float.abs ((x * Float.ofNat a) - Float.round (x * Float.ofNat a)) < 1e-4 diff --git a/src/denom.py b/src/denom.py deleted file mode 100644 index b18db2d..0000000 --- a/src/denom.py +++ /dev/null @@ -1,4 +0,0 @@ -x = 1 - 0.9772532922866427 -for i in range(1, 10000): - if abs(x * i - round(x * i)) < 1e-4: - print(i, x * i) |