visualize arxiv papers using lean

gistfile1.txt

#%% 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:
    for line in f:
        try:
            paper = json.loads(line)
        except json.JSONDecodeError:
            continue

        title = paper.get("title") or ""
        abstract = paper.get("abstract") or ""
        comments = paper.get("comments") or ""
        text = title + " " + abstract + " " + comments

        if re.search(r"\blean\b", text, re.IGNORECASE):
            papers_with_lean.append(paper)

print(f"Total papers containing the word 'lean': {len(papers_with_lean)}")

#%% For each paper, extract and print the sentence(s) containing "lean"
# This lets us manually inspect which uses refer to the Lean theorem prover

for paper in papers_with_lean:
    pid = paper.get("id", "?")
    title = (paper.get("title") or "").replace("\n", " ").strip()
    abstract = (paper.get("abstract") or "").replace("\n", " ").strip()
    comments = (paper.get("comments") or "").replace("\n", " ").strip()

    # Split into sentences (rough heuristic)
    full_text = title + ". " + abstract + " " + comments
    sentences = re.split(r"(?<=[.!?])\s+", full_text)

    matching_sentences = [
        s.strip() for s in sentences if re.search(r"\blean\b", s, re.IGNORECASE)
    ]

    print(f"\n[{pid}] {title}")
    for s in matching_sentences:
        print(f"  >>> {s}")

#%% Now filter: keep only papers where "lean" refers to the Lean theorem prover
# Strategy: match Lean 3, Lean 4, Lean prover, Lean proof assistant,
#           or Lean near formalization/mathlib/theorem-proving keywords

lean_prover_papers = []

for paper in papers_with_lean:
    title = (paper.get("title") or "").replace("\n", " ")
    abstract = (paper.get("abstract") or "").replace("\n", " ")
    comments = (paper.get("comments") or "").replace("\n", " ")
    text = (title + " " + abstract + " " + comments).lower()

    # Direct mentions of Lean as a prover
    is_lean_prover = (
        bool(re.search(r"\blean\s*[34]\b", text))
        or bool(re.search(r"\blean\s+(theorem\s+)?prover\b", text))
        or bool(re.search(r"\blean\s+proof\s+assistant\b", text))
        or bool(re.search(r"\bmathlib\b", text))
        or bool(re.search(r"\blean'?s?\s+math", text))
        # "in Lean" or "using Lean" near formalization keywords
        or bool(
            re.search(
                r"(formal|verif|proof|theorem|tactic|interactive).{0,80}\blean\b", text
            )
        )
        or bool(
            re.search(
                r"\blean\b.{0,80}(formal|verif|proof|theorem|tactic|interactive)", text
            )
        )
    )

    # Exclude known false positives: "lean manufacturing", "lean body", "lean mass",
    # "lean tree", "lean and", "lean mixture", etc.
    is_false_positive = bool(
        re.search(
            r"\blean\s+(manufactur|body|mass|mixture|burn|tree|decomposition|startup|management|enterprise|agile|six\s*sigma|production|supply|process|operation|principle|thinking|approach(?!\s+to\s+(formal|verif|proof)))",
            text,
        )
    )

    if is_lean_prover and not is_false_positive:
        lean_prover_papers.append(paper)

print(f"\nPapers using Lean (theorem prover) for formalization: {len(lean_prover_papers)}")

#%% Print all Lean prover papers with their matching sentences for verification

for paper in lean_prover_papers:
    pid = paper.get("id", "?")
    title = (paper.get("title") or "").replace("\n", " ").strip()
    abstract = (paper.get("abstract") or "").replace("\n", " ").strip()
    comments = (paper.get("comments") or "").replace("\n", " ").strip()
    categories = paper.get("categories", "")
    update_date = paper.get("update_date", "")

    full_text = title + ". " + abstract + " " + comments
    sentences = re.split(r"(?<=[.!?])\s+", full_text)
    matching_sentences = [
        s.strip() for s in sentences if re.search(r"\blean\b", s, re.IGNORECASE)
    ]

    print(f"\n[{pid}] {title}")
    print(f"  categories: {categories}  date: {update_date}")
    for s in matching_sentences:
        print(f"  >>> {s}")

#%% Summary: count by year (math papers only)

from collections import Counter
import matplotlib.pyplot as plt

year_counts_all = Counter()
year_counts_math = Counter()
year_counts_math_primary = Counter()
for paper in lean_prover_papers:
    date = paper.get("update_date", "")
    if not date:
        continue
    year = date[:4]
    year_counts_all[year] += 1
    cats = (paper.get("categories") or "").split()
    if any(c.startswith("math.") for c in cats):
        year_counts_math[year] += 1
    # Check if primary category (first one) is math.*
    if cats and cats[0].startswith("math."):
        year_counts_math_primary[year] += 1

print("\nLean prover papers by year (math.* only):")
for year in sorted(year_counts_math):
    print(f"  {year}: {year_counts_math[year]}")
print(f"  TOTAL: {sum(year_counts_math.values())}")

print("\nLean prover papers by year (primary category math.*):")
for year in sorted(year_counts_math_primary):
    print(f"  {year}: {year_counts_math_primary[year]}")
print(f"  TOTAL: {sum(year_counts_math_primary.values())}")

print("\nLean prover papers by year (all):")
for year in sorted(year_counts_all):
    print(f"  {year}: {year_counts_all[year]}")
print(f"  TOTAL: {sum(year_counts_all.values())}")

#%% Plot: Lean formalization papers by year

all_years = sorted(set(year_counts_all) | set(year_counts_math) | set(year_counts_math_primary))
counts_all = [year_counts_all[y] for y in all_years]
counts_math = [year_counts_math[y] for y in all_years]
counts_math_primary = [year_counts_math_primary[y] for y in all_years]

fig, ax = plt.subplots(figsize=(10, 3), dpi=300)
bar_width = 0.25
x = range(len(all_years))
ax.bar([i - bar_width for i in x], counts_all, bar_width, label=f"All Lean prover papers ({sum(counts_all)})")
ax.bar([i for i in x], counts_math, bar_width, label=f"math.* papers (any category) ({sum(counts_math)})")
ax.bar([i + bar_width for i in x], counts_math_primary, bar_width, label=f"math.* papers (primary category) ({sum(counts_math_primary)})")

ax.set_xlabel("Year")
ax.set_ylabel("Number of papers")
ax.set_title("ArXiv papers using Lean for formalization, by year")
ax.set_xticks(list(x))
ax.set_xticklabels(all_years)
ax.legend()
for i, (a, m, mp) in enumerate(zip(counts_all, counts_math, counts_math_primary)):
    ax.text(i - bar_width, a + 1, str(a), ha="center", fontsize=7)
    ax.text(i, m + 1, str(m), ha="center", fontsize=7)
    ax.text(i + bar_width, mp + 1, str(mp), ha="center", fontsize=7)
plt.tight_layout()
plt.show()

#%% Category breakdown: math vs CS

math_only = 0
cs_only = 0
both_math_cs = 0
neither = 0

for paper in lean_prover_papers:
    cats = (paper.get("categories") or "").split()
    has_math = any(c.startswith("math.") for c in cats)
    has_cs = any(c.startswith("cs.") for c in cats)

    if has_math and has_cs:
        both_math_cs += 1
    elif has_math:
        math_only += 1
    elif has_cs:
        cs_only += 1
    else:
        neither += 1

total = len(lean_prover_papers)
print("\nCategory breakdown of Lean prover papers:")
print(f"  math.* only:        {math_only}")
print(f"  cs.* only:          {cs_only}")
print(f"  Both math.* & cs.*: {both_math_cs}")
print(f"  Neither:            {neither}")
print()
print(f"  Has any math.* category: {math_only + both_math_cs}  ({100*(math_only + both_math_cs)/total:.1f}%)")
print(f"  Has any cs.* category:   {cs_only + both_math_cs}  ({100*(cs_only + both_math_cs)/total:.1f}%)")

#%% Category distribution (all categories)

all_subcats = Counter()
for paper in lean_prover_papers:
    cats = (paper.get("categories") or "").split()
    for c in cats:
        all_subcats[c] += 1

print("\nAll categories among Lean prover papers:")
for cat, count in all_subcats.most_common():
    print(f"  {cat}: {count}")

#%% Sunburst chart of categories


import plotly.express as px
import pandas as pd

# Build dataframe with primary category breakdown
# Top level: math vs cs vs other (based on primary category)
# Second level: subcategory
MIN_COUNT = 4

rows = []
for paper in lean_prover_papers:
    cats = (paper.get("categories") or "").split()
    if not cats:
        continue
    primary = cats[0]  # Primary category is the first one
    if '.' in primary:
        parent = primary.split('.')[0]
        subcat = primary
    else:
        parent = primary
        subcat = primary

    rows.append({
        'parent': parent,
        'subcat': subcat,
        'count': 1
    })

df = pd.DataFrame(rows)

# Group by parent and subcat, count papers
df_grouped = df.groupby(['parent', 'subcat']).sum().reset_index()

# Group small subcategories into "other"
subcat_counts = df_grouped.groupby('subcat')['count'].sum()
df_grouped['subcat_display'] = df_grouped.apply(
    lambda row: row['subcat'] if subcat_counts[row['subcat']] >= MIN_COUNT else f"{row['parent']}.other",
    axis=1
)

# Re-aggregate after grouping into "other"
df_final = df_grouped.groupby(['parent', 'subcat_display'])['count'].sum().reset_index()
df_final.columns = ['parent', 'subcat', 'count']

fig = px.sunburst(
    df_final,
    path=['parent', 'subcat'],
    values='count',
    title="ArXiv primary categories of Lean prover papers",
)
fig.update_traces(textinfo='label+value')
fig.update_layout(width=600, height=600)
fig.show()

import plotly.io as pio
pio.write_image(fig, "lean_prover_papers_categories.png", scale=3)

# %%