Alexander Comerford cmrfrd

➗

Just doing the beep boop

Stuck at the junction of Data Science, Infrastructure, and Cryptography 📐 @nearai prev: @coinbase, @bloomberg

cmrfrd / prop.py

Created June 16, 2025 03:00

https://xpuzzlecorner.substack.com/p/oceans-4

	import random
	import math
	from collections import Counter

	def sample_unit_circle(n) -> list[tuple[float, float]]:
	points = []
	while len(points) < n:
	x = random.uniform(-1, 1)
	y = random.uniform(-1, 1)
	if xx + yy <= 1:

cmrfrd / friday_13th.lean

Last active June 18, 2025 01:09

A lean4 proof showing there will always be at least 1 friday the thirteenth per year. Try in https://live.lean-lang.org/

	import Mathlib.Data.ZMod.Basic
	import Mathlib.Data.Fin.Basic
	import Mathlib.Tactic.IntervalCases
	import Mathlib.Tactic
	import Mathlib.Tactic.FinCases
	import Mathlib.Data.Fintype.Basic
	import Mathlib.Data.Finset.Basic
	import Mathlib.Data.Finset.Card

	/-!

cmrfrd / rat_dense.lean

Created July 18, 2025 21:44

lean proof of density of the rationals

	import Mathlib.Tactic
	import Mathlib.Algebra.Field.Basic
	import Mathlib.Topology.Basic
	import Mathlib.Topology.Order.Basic
	import Mathlib.Data.Real.Basic
	import Mathlib.Data.Real.Basic
	import Mathlib.Data.Rat.Defs
	import Mathlib.Data.Int.Cast.Lemmas
	import Mathlib.Topology.MetricSpace.Basic
	import Mathlib.Topology.Constructions