Vilin97

import Mathlib

namespace dyadic

-- k/2^n
inductive Dyadic where
  | zero    : Dyadic
  | add_one : Dyadic → Dyadic  -- x ↦ x + 1
  | half    : Dyadic → Dyadic  -- x ↦ x / 2
  | neg     : Dyadic → Dyadic  -- x ↦ -x

Vilin97

import Mathlib

namespace HW_III_6

universe u

inductive MyEq {α : Sort u} : α → α → Prop where
  | refl a : MyEq a a

#check MyEq 1 2

Vilin97

#!/usr/bin/env python3
"""
Reconstruct the true PutnamBench SOTA timeline by combining:
1. Git commit history of results.json (for models added in real time)
2. Manual corrections for models whose paper/announcement dates differ
   from when they were added to the leaderboard.

Saves CSV and generates a plot.
"""

Vilin97

import { useState, useRef, useCallback, useEffect } from "react";

/* ─── constants ─── */
const LOADING_PHRASES = [
  "Digging through the archives…",
  "Unearthing forgotten scandals…",
  "Consulting dusty manuscripts…",
  "Interviewing ghosts…",
  "Decoding secret diaries…",
];

Vilin97

#%% Imports and setup
import json
import re

DATA_PATH = "arxiv-metadata-oai-snapshot 2.json"

#%% Load all papers that contain the word "lean" (case-insensitive) anywhere in title/abstract/comments
papers_with_lean = []

with open(DATA_PATH, "r") as f:

Vilin97

#%% Imports and setup
import json
import re

DATA_PATH = "arxiv-metadata-oai-snapshot.json"

#%% Load all papers that contain the word "lean" (case-insensitive) anywhere in title/abstract/comments
papers_with_lean = []

with open(DATA_PATH, "r") as f:

Vilin97

"reset a leaf"
function reset!(leaf::Leaf{A, S}) where {A <: Optimisers.Adam, S}
    leaf.state[1] .= 0
    leaf.state[2] .= 0
    leaf.state = (leaf.state[1], leaf.state[2], leaf.rule.beta)
    nothing
end
"reset optimiser state"
function reset!(state::NamedTuple{(:layers,), L}) where {L}
    for layer in state.layers

Vilin97

using DiffEqJump, Random, BenchmarkTools, DataStructures
const MINJUMPRATE = 2.0^exponent(1e-12)

function pq_setup(rates)
    pqdata = randexp(length(rates))./rates
    MutableBinaryMinHeap(pqdata)
end

function pt_setup!(pt, rates)
    DiffEqJump.reset!(pt)

Vilin97

\DeclarePairedDelimiter{\norm}{||}{||_1}
\providecommand{\floor}[1]{\left \lfloor #1 \right \rfloor }
\newcommand{\shortexactseq}[5]{#1\to #2 \hookrightarrow #3 \twoheadrightarrow #4 \to #5}
\newcommand{\rad}[1]{\sqrt{#1}}
\newcommand{\set}[1]{\left\{ #1 \right\}}
\newcommand{\gen}[1]{\langle #1 \rangle}
\newcommand{\restr}[1]{|_{#1}}
\newcommand{\sepdeg}[2]{[{#1}:{#2}]_{\rm sep}}

\renewcommand{\Pr}{\mathbb{P}}