utensil

Formal fidelity audit of 34 selected mathematical claims

This report examines statement alignment, definition fidelity, executed proof checks, and correspondence with manuscript arguments. It covers 30 openai/math manuscripts, two separate OpenAI fluids papers, and two external comparison works. The cohort is identified in the 34-result source survey. The audit concerns the pinned sources and checks completed on October 8, 2026.

15 claims have matching formal source statements, 4 have only supporting or related companion targets, and 15 have no corresponding artifact identified in the inspected materials. Fourteen source matches are at the original snapshot; the fifteenth is a later logspace target. Navier–Stokes counts as a source match because its full construction appears in the formal source, although its configured Comparator statements are narrower.

All 20 original configurations w

utensil

This report grades and ranks selected mathematical contributions in openai/math under the convex-hull grading standard.

Grade and rank report — October 8, 2026

Overview

All 30 contributions receive 0.5: methodological development within an inherited conceptual framework, including substantial new proof methods. The cohort contains 30 openai/math manuscripts. Separately released OpenAI papers and external comparison works are excluded.

All 435 pairs are compared. The list has 28 ordered ranks, with two ties; entries within a joint rank are not ordered. Comparative confidence is generally low to moderate. The companion ledger contains the pairwise reasons and reversal tests.

utensil

Convex hull grading standard for mathematical contributions

This standard evaluates the originality of mathematical contributions in the AI era. It is motivated by the convex-hull metaphor for AI's mathematical capabilities: can AI only work within the reach of accumulated human mathematics, or can it introduce fundamentally new mathematical ideas?

Here the convex hull of human mathematical knowledge means, metaphorically, the reach of the concepts, perspectives, methods and techniques that human mathematicians have established at a specified historical cutoff, including

utensil

{
  "$schema": "https://zed.dev/schema/themes/v0.1.0.json",
  "name": "Railscasts Renewed",
  "author": "Utensil Song",
  "themes": [
    {
      "name": "Railscasts Renewed Dark",
      "appearance": "dark",
      "style": {
        "background.appearance": "opaque",

utensil

Github to Discord Webhook Tutorial

In this tutorial I'll show you how to create a Github webhook that will post updates from your Github account to a channel in Discord. The steps are simple so follow along!

Create a Webhook in a Discord Channel

First you need to create a webhook in a text channel. We're assuming you have both Manage Channel and Manage Webhooks permissions!

• Go in a channel properties (Alternatively, Server Settings, Webhooks works too)

utensil

import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

set_option pp.proofs.withType false

variable {R M} [CommRing R] [Invertible (2 : R)] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M)

abbrev ExteriorAlgebra.rMultivector (r : ℕ) : Submodule R (ExteriorAlgebra R M) :=
  (LinearMap.range (ExteriorAlgebra.ι R : M →ₗ[R] _) ^ r)

utensil

/-

This file demonstrates the use of VSCode [Spell Right](https://marketplace.visualstudio.com/items?itemName=ban.spellright)
extension to spell check comments in Lean 4 files while avoiding code or code blocks in comments, it uses some heuristics
to work for both Markdown and [reStructuredText](https://devguide.python.org/documentation/markup/) per request on
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Spell.20check).

The minimal configuration to make it work for Lean is to add the following to your `settings.json` after the installing
the extension, setting up [the spell check dictionaries](https://github.com/bartosz-antosik/vscode-spellright#dictionaries),
and [enable spell check for the language of your choosing](https://github.com/bartosz-antosik/vscode-spellright#changing-language-and-turning-off):

utensil

/*

You may use it via https://github.com/openstyles/stylus/ , matching url prefix: https://live.lean-lang.org/

*/

/*

Code for dark style of the Monaco editor

utensil

Why formalize? Why Lean?

Why should mathematicians care about formalization?

Why Lean might be a better choice for mathematicians?

Quotes from CICM 2020 Slack chat log

Can we get one system which is capable of understanding all of the mathematics in my university's undergraduate pure maths degree?

utensil

Basic guide to tactics

This guide might be of use when you are in a situation where you know exactly what you want to do "in real life" in your proof, but don't know how to do it in Lean. For example, you might be faced with a hypothesis of the form p ∧ q and you need a proof of p, or you might be faced with a goal of the form p ∨ q which you want to deduce from a proof of p.

How to use the guide

Let's say that you know your next step involves p ∧ q in some way. Which tactic you use depends on whether p ∧ q is a hypothesis (i.e. you have the assumption H : p ∧ q in your local context) or the goal (i.e. what you are trying to prove). If it is a hypothesis then you need to eliminate it, whereas if it is the goal then you need to introduce it

Once you have established whether you want to introduce or eliminate it, find the function in the list below and you will see the tactic you need. Click on the link to see an example of usage.