Instantly share code, notes, and snippets.

# Thomas Chaumeny tchaumeny

Last active January 10, 2024 06:28
A Lean proof of the chocolate tablet theorem
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 -- Chocolate Bar Theorem 🍫, as illustrated in https://www.instagram.com/p/CzGr1yfAHFB/ -- Credits: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Formulating.20the.20chocolate.20bar.20theorem -- Run on https://live.lean-lang.org/ import Mathlib.Data.Nat.Basic inductive ChocoTablet : Nat -> Nat -> Type where | square : ChocoTablet 1 1 | hJoin {a b b' : Nat} : ChocoTablet a b -> ChocoTablet a b' -> ChocoTablet a (b + b')
Last active January 6, 2024 09:34
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 from automathon import DFA from collections import defaultdict from itertools import zip_longest from math import floor from random import randint # See https://www21.in.tum.de/teaching/sar/SS20/9.pdf def ineq_to_dfa(A: list[int], b: int) -> DFA: n = len(A)
Last active March 29, 2023 22:07
Compute Goodstein's sequences — https://lipsum.dev/2023-03-1-logique-arithmetiques-completude/
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 from typing import Iterator HereditaryRepresentation = list[tuple[int, "HereditaryRepresentation"]] def to_base(n: int, base: int, prefix: bool = False) -> list[int]: """ Computes the representation of n in the specified base. """ if n == 0:
Last active January 31, 2023 19:04
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 // See lipsum.dev import React, { useEffect, useRef, useState } from "react"; const L = 8; function baseFunc(u, v) { return (x, y) => Math.cos(((2 * x + 1) * u * Math.PI) / 16) * Math.cos(((2 * y + 1) * v * Math.PI) / 16);
Last active December 28, 2022 20:57
Basic FFT implementation, see https://lipsum.dev/2022-12-28-fft-multiplication-polynomials/
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 # See https://mitpress.mit.edu/9780262046305/introduction-to-algorithms/, chapter 30 # /!\ Do not use it in production /!\ from math import e, pi import numpy as np from numpy.testing import assert_array_equal def fft(L, sign=-1):
Created July 15, 2021 19:34
Implementation of Fermat and Miller-Rabin tests in Python, see https://lipsum.dev/2021-06-1-miller-rabin-openssl/
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 # Part of https://lipsum.dev/2021-06-1-miller-rabin-openssl/ # /!\ Warning /!\ — Not safe for real cryptographic usage from collections import Counter from random import randrange import statistics # Fermat def fermat_test(n, max_witness=100):
Last active October 10, 2020 12:17
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 // RotatingCube React component, used in https://lipsum.dev/2020-09-1-rotations/ import * as BABYLON from 'babylonjs' import * as GUI from 'babylonjs-gui' import React, { useEffect, useRef, useState } from 'react' const canvasWidth = 500; const canvasHeight = 300; function initScene(canvas, rotationCb) { const engine = new BABYLON.Engine(canvas);
Last active May 24, 2020 13:13
Polynomial type in Python
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 # See https://lipsum.dev/2020-05-1-pourquoi-les-polynomes/ from numbers import Number class Polynomial: def __init__(self, *coefficients): self.degree = -1 self.coefficients = tuple(coefficients) for i, coef in enumerate(self.coefficients): if coef != 0:
Last active February 17, 2017 21:51
Converting amount of money (including cents) to words using num2words
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 from num2words import num2words def money_amount_words(amount, units='euros', cents='centimes', lang='fr'): """ Returns an iterator over the words describing the given amount Args: amount: decimal.Decimal, the amount of money units: str, the currency units