Contributing

Small, explicit interfaces make the library easier to reuse. Open a focused change with its mathematical statement, assumptions and a compiling consumer.

• Keep the Lean toolchain and Mathlib pin consistent. Verify source changes locally first.
• Provide a real positive example and a meaningful strict negative control when a mathematical constant, sign or domain boundary changes.
• Preserve source provenance and the Apache-2.0 license. Distinguish known-theorem formalization from new mathematics.
• Update all public entrypoints when claim scope changes; do not describe draft or unaccepted evidence as released.

Full clone-local guidance: CONTRIBUTING.md and AGENTS.md.