THIS IS EXPERIMENTAL FOR NOW

Features to add:

• form to allow contribution suggestions
• conjecture upvoting system?

Website for the Formal Conjectures Lean 4 repository.

The site is a static website generated from a JSON metadata file produced by the formal-conjectures repository. The overall data flow is:

formal-conjectures repo (Lean 4)
  └─ lake exe extract_names
       └─ data/conjectures.json   ← added here by formal-conjectures CI
            └─ node build.js
                 └─ site/         ← deployed to GitHub Pages

1. Data extraction. The formal-conjectures CI runs lake exe extract_names (defined in scripts/extract_names.lean). This imports all compiled Lean modules, reads the @[category] and @[AMS] attributes, and writes a JSON array to stdout. Each entry contains the theorem's fully-qualified name, module, category, AMS subject codes, pretty-printed statement, and docstring.

2. Data creation. The formal-conjectures CI adds the resulting JSON to data/conjectures.json in this repository.

3. Site build. A push to data/conjectures.json triggers this repo's GitHub Actions workflow (.github/workflows/deploy.yml), which runs node build.js and deploys the output to GitHub Pages.

During the site build, build.js also reads the repository's git history to attach file-level contributor metadata to each theorem page. If GITHUB_TOKEN or GH_TOKEN is available, the build enriches matching contributors with their GitHub username, profile URL, and avatar URL; otherwise it falls back to the display names available in git history.

data/
  conjectures.json        # JSON produced by lake exe extract_names (created by CI)
src/
  css/style.css           # Stylesheet (CSS custom properties throughout)
  js/
    main.js               # Shared utilities loaded on every page
    browse.js             # Filter/search/paginate logic for /browse/
    theorem.js            # Theorem detail rendering for /theorem/
  templates/
    index.html            # Landing page template (stats injected by build.js)
    browse.html           # Browse page (client-side filtering)
    theorem.html          # Theorem detail page (client-side, reads ?name= param)
    contribute.html       # How-to-contribute page (static)
    about.html            # About page (static)
    team.html             # Team page (static)
build.js                  # Build script — reads data/, writes site/
package.json
.github/workflows/
  deploy.yml              # CI: build + deploy to GitHub Pages

The site/ output directory is generated by the build script and is not committed (it is in .gitignore).

Individual theorem pages are rendered client-side from data/conjectures.json — no separate HTML file is generated per theorem.

Lean code uses Verso's existing tokens and hover information. The shared theme, src/css/lean-syntax.css, maps VS Code Light+ colors to Verso's CSS variables and token classes.

Our verso-html renderer accepts only input and output directories, so fix_literate_html.py installs the stylesheet in generated source pages. Theorem excerpts load the same stylesheet from the website assets. Run the post-processor again after changing the theme to refresh source previews.

The quickest way to develop the website locally is using dev.sh, which downloads the conjectures data from the live production site (no Lean build needed):

Requirements: Node.js 18+ and Python 3.

# Install Node.js if needed (e.g. via conda)
conda install -c conda-forge nodejs

# Build and serve
cd site
./dev.sh              # build + serve on http://localhost:8080
./dev.sh --build-only # just build, no server
./dev.sh --port 3000  # serve on a custom port

To iterate on templates or styles, re-run ./dev.sh --build-only after each change and refresh the browser.

If you need the site to reflect local Lean changes (new conjectures, etc.):

# In the formal-conjectures repo root
lake exe cache get   # download prebuilt Mathlib oleans (first time only)
lake build
mkdir -p site/data
lake exe extract_names --exclude=statement,docstring,moduleDocstrings,fileFirstAdded,fileLastModified > site/data/conjectures.json

# (Optional) Generate Verso literate fragments for rendered docstrings.
# Without this, theorem detail pages will lack formatted docstrings and source links.
# Warning: the literate build step can take a long time (30+ minutes).
cd docbuild
lake build FormalConjectures:literate FormalConjecturesForMathlib:literate FormalConjecturesUtil:literate
lake exe verso-html .lake/build/literate ../_literate_html
cd ..
python3 site/fix_literate_html.py _literate_html
python3 site/extract_verso_fragments.py _literate_html site/data/verso-fragments.json

# Build the site
cd site
node build.js        # output goes to site/

# Serve locally
python3 -m http.server 8080 --directory site

To share a live preview of your website changes with others, you can deploy from a *-webtest branch on your GitHub fork. The CI workflow detects this naming convention and skips the slow Lean build, downloading data from the live production site instead.

1. Fork the repository on GitHub.

2. Enable GitHub Pages:

   • Go to your fork's Settings → Pages
   • Set Source to GitHub Actions

3. Allow webtest branches to deploy:

   • Go to Settings → Environments → github-pages
   • Under Deployment branches and tags, click Add deployment branch or tag rule
   • Add the pattern *-webtest
   • Save

# Create a webtest branch from main
git checkout -b my-feature-webtest origin/main

# Make your website changes (CSS, JS, templates, etc.)
# ...

# Push to your fork — CI builds and deploys automatically
git push <your-fork> my-feature-webtest

Your site will be live at https://<username>.github.io/formal-conjectures/ once the Action completes (typically ~2 minutes for a website-only build).

Note: The naming convention *-webtest is what triggers the fast website-only build. Branches without this suffix run the full Lean build.

Note: GitHub Pages serves one deployment at a time per repo. Deploying from a webtest branch replaces what was deployed from main. This is fine for a fork used for previewing.

The GitHub Actions workflow in .github/workflows/build-and-docs.yml triggers on pushes to main and *-webtest branches, as well as on pull requests.

Build modes:

Deployment happens on pushes to main, and on *-webtest branches when on a fork.

For GitHub Pages setup (including the environment rule needed for *-webtest branches), see One-time fork setup above.