Formal Conjectures

The WrittenOnTheWallII directory contains a selection of graph conjectures from the WOWII database. Each conjecture is provided as a Lean file containing the formal statement of the conjecture along with placeholder proofs.

Conjectures are categorized by their status as either open or resolved. This collection serves as a grouping of mathematical statements intended for formal verification.

The repository is organized by the source of the conjectures. It includes two specialized directories:

• FormalConjecturesUtil: Contains project-specific utilities, including the category attribute, the answer( ) elaborator, and various linters.
• FormalConjecturesForMathlib: Contains code intended for potential upstreaming to mathlib. This directory follows the standard mathlib directory structure.

Note that the project uses specific attributes like @[category], @[formal_proof], and @[AMS], as well as the answer( ) elaborator to manage conjecture statements.

The worker uses a Cloudflare KV namespace named VOTES to persist data.

• Key format: votes:{theoremName}
• Value format:

{
  "count": N, 
  "voters": ["user1", "user2"], 
  "ratings": { "user1": 7, "user3": 4 }
}

Logic Details:

• Deduplication: The voters array ensures each GitHub user can only vote once per theorem.
• Ratings: The ratings object maps GitHub logins to difficulty values (0–10 integers).
• Cleanup: When the last voter removes their vote and no ratings remain, the KV key is deleted.

Voting Logic

• Single Vote: Users can toggle a like/unlike state once per theorem.
• Deduplication: The system prevents duplicate votes by maintaining a voters array within the Cloudflare KV value.
• Cleanup: If a vote is removed and no votes or ratings remain for a theorem, the corresponding KV key is deleted.

Difficulty Ratings

• Scale: Users rate theorem difficulty on a scale of 0–10.
• Overwrite Behavior: Users can submit a rating once; subsequent submissions overwrite the previous rating.
• UI Integration:
  • The browse page displays the average difficulty alongside the total vote count.
  • The theorem detail page provides a dropdown for rating and shows the current average.

The voting and difficulty rating system operates through a client-server model where the browser interacts with a Cloudflare Worker. The worker manages OAuth token exchange, CRUD operations for votes and difficulty ratings, and persists data in Cloudflare KV storage.

Architecture Flow:

• Browser (voting.js): Initiates operations and handles GitHub OAuth identity verification.
• Cloudflare Worker (worker/): Acts as the backend, performing OAuth exchanges and managing data.
• Cloudflare KV: Provides the storage layer for votes and ratings.

Note that GitHub OAuth is used strictly for identity verification with zero permissions requested. The browser only makes a call to the GitHub /user endpoint to fetch the username during the login process.

The repository provides immutable stable benchmark snapshots tagged with the format bench-v{N}-lean4.{X}.{Y}.

• v{N} (Benchmark version): Represents the specific set of problems included. This version is incremented whenever problems are added, removed, or misformalisations are corrected.
• lean4.{X}.{Y} (Lean version): Identifies the specific Lean 4 toolchain version used for that snapshot.

Because tags are immutable, any fixes to misformalisations will result in a new benchmark version (v{N+1}) rather than a patch to an existing one.

Follow these steps to run the voting system locally:

1. Register a GitHub OAuth App at https://github.com/settings/developers:
   • Set the callback URL to your local development URL (e.g., http://localhost:8000).
   • Important: Do NOT request any scopes (ensure zero permissions).
2. Set up the worker: Follow the instructions in worker/README.md to create KV namespaces, set secrets, and configure local development.
3. Update voting.js constants:
   • Set WORKER_URL to http://localhost:8787.
   • Set GH_CLIENT_ID to your app's client ID.
4. Start the worker:

   cd worker && npm run dev

5. Build and serve the site:

   npm run build && cd site && python3 -m http.server 8000

Local Development

Start a local development server (default http://localhost:8787) using:

npm run dev

For local development, create a .dev.vars file to store your secrets:

GH_CLIENT_ID=your_client_id
GH_CLIENT_SECRET=your_client_secret

Deployment

Deploy the worker to Cloudflare using:

npm run deploy

Follow these steps to install dependencies, create the required KV storage, and configure secrets for the Cloudflare Worker.

1. Install Dependencies

cd worker
npm install

2. Create KV Namespace

Create a KV namespace named VOTES for production and preview environments:

npx wrangler kv namespace create VOTES
npx wrangler kv namespace create VOTES --preview

Copy the resulting IDs into your wrangler.toml file:

[[kv_namespaces]]
binding = "VOTES"
id = "<production-id>"
preview_id = "<preview-id>"

3. Configure Secrets

Store your GitHub OAuth credentials as Cloudflare Worker secrets:

npx wrangler secret put GH_CLIENT_ID
npx wrangler secret put GH_CLIENT_SECRET

4. Configure CORS

Update the ALLOWED_ORIGIN variable in wrangler.toml to match your deployed site URL to ensure correct CORS behavior.