Skip to content

Instantly share code, notes, and snippets.

View char3210's full-sized avatar

Char char3210

View GitHub Profile
@char3210
char3210 / redpoints.lean
Created February 27, 2026 23:03
Lean 4 formal proof of OMA 2023 Regional Level 2, Problem 1
import Mathlib
def InRect (p : ℚ × ℚ) : Prop :=
0 ≤ p.1 ∧ p.1 ≤ 28 ∧
0 ≤ p.2 ∧ p.2 ≤ 14
def dist_sq (p q : ℚ × ℚ) : ℚ :=
(p.1 - q.1)^2 + (p.2 - q.2)^2
@char3210
char3210 / 10.rs
Created December 11, 2025 05:50
advent of code 2025 day 10 solution in rust (no libraries or floats)
#![allow(nonstandard_style)]
use std::{array, fmt::{Debug, Display}, i32, ops::{AddAssign, Deref, DerefMut, Index, IndexMut, Mul, SubAssign}, u64};
advent_of_code::solution!(10);
pub fn part_one(input: &str) -> Option<u64> {
let mut sum = 0;
for line in input.lines() {
let split: Vec<_> = line.split(" ").collect();
let mut chars = split[0].chars();
@char3210
char3210 / word_pair_hash_collisions.rs
Last active September 28, 2025 00:29
Given a dictionary, efficiently searches for pairs of words in the form "word1 word2" matching a specific hash with Java's String hash function
use std::{collections::HashMap, env::args, fs};
use num_bigint::BigInt;
fn h0(s: &str) -> i32 {
let mut h = 0i32;
for b in s.bytes() {
h = h.wrapping_mul(31).wrapping_add(b as i32);
}