jsmorph

GPT 5.4 compiled these instructions from this blog post by Scott Armstrong about his and Julia Kempe's Lean 4 formalization of De Giorgi–Nash–Moser theory.

Armstrong's recent math formalization notes (as interpreted)

This skill is for formalization projects in mature parts of

kim-em

ZEN Mathematics Center: New Project "LANA" Announcement

ZEN大学「ZMC（ZEN Mathematics Center; ZEN数学センター）」新プロジェクト「LANA」の発表

• Date: March 31, 2026
• Video: https://www.youtube.com/live/b9ZV-4T3iUo
• Duration: 1h 24m (first ~11 minutes are pre-stream holding screen)
• Language: Japanese (with some English from online participants, consecutively translated)

English Summary

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.
"""

karpathy

"""
The most atomic way to train and run inference for a GPT in pure, dependency-free Python.
This file is the complete algorithm.
Everything else is just efficiency.

@karpathy
"""

import os       # os.path.exists
import math     # math.log, math.exp

FaffyWaffles

import Mathlib

open scoped BigOperators
open Filter
open scoped Nat

namespace Real

/-
============================================================

llllvvuu

import Mathlib

set_option linter.style.longLine false

open Set Filter Topology RealInnerProductSpace Gradient

variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (f : V → ℝ) (X : ℝ → V) (r : ℝ)

def minimizers : Set V := {x | IsMinOn f Set.univ x}

vgel

import argparse
import random
import sys

from transformers import AutoModelForCausalLM, AutoTokenizer, DynamicCache
import torch

parser = argparse.ArgumentParser()
parser.add_argument("question", type=str)
parser.add_argument(

yoavg

Are multi-LLM-agent systems a thing? Yes they are. But.

Yoav Goldberg, Nov 24, 2024

This piece started with a pair of twitter and bluesky posts:

let's talk about "agents" (in the LLM sense). there's a lot of buzz around "multi-agent" systems where agents collaborate but... i don't really get how it differs from a thinking of a single agent with multiple modes of operation. what are the benefits of modeling as multi-agent?

— (((ل()(ل() 'yoav))))👾 (@yoavgo) November 23, 2024

seewoo5

chrisflav

import Mathlib.RingTheory.RingHom.FinitePresentation
import Mathlib.RingTheory.Flat.Algebra
import Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

/-!
Authors: Judith Ludwig, Christian Merten

Note: This only works on the mathlib branch chrisflav/finpres.2
-/