# Math Research Collaborator
A research workflow and execution toolkit for mathematicians collaborating with AI through natural language. The host AI takes initiative in implementation, proposals and critique. Statements, assumptions, proofs and evidence stay together.
**[Open the English interface](https://nclamvn.github.io/math-research-collaborator/?lang=en)** · **[Download a release](https://github.com/nclamvn/math-research-collaborator/releases)** · **[Tiếng Việt](README.vi.md)**
## Start with a mathematical question
Extract the complete release and open its folder in a tool-enabled AI workspace. Ask:
> Read AGENTS.md, adopt this research workflow, check prerequisites and run acceptance. Then investigate my mathematical question: [your question]. I will communicate in natural language. Take responsibility for implementation, critique, verification and evidence-backed reporting.
The mathematician should not have to write JSON, operate Lean commands or edit registries. The host must actually support file access and command execution. Attaching a ZIP to a text-only conversation does not enable proof checking.
Open `index.html` or `START_HERE.html` locally for the offline interface. It switches fully between Vietnamese and English, explains the method, displays actual proofs and audit output, documents readiness and prepares a research brief for copying or downloading. It does not run Lean or call an AI service inside the browser.
## What is implemented
| Component | Implemented behavior |
|---|---|
| Research dossiers | Projects, immutable claims, sources, snapshots, notes, decisions and next steps |
| Proof attempts | Fixed Lean/Std propositions, bounded retries, diagnostics and transitive axiom auditing |
| Refutation | Checked exact negations linked to the original proposition |
| Exploration | Named variants with an explicit relationship to the original goal |
| Concrete LRC adapter | Exact modular witness search, checkpoint recovery and Lean checking |
| Transfer | Export, non-overwriting import and fresh-directory proof replay |
| Recipient acceptance | 14 backend scenarios, including failed and repaired proofs and evidence drift |
| Bilingual interface | Six views; desktop/mobile tests; no runtime network requests |
## Readiness and limitations
This is a transferable release candidate with locally tested execution. It has not undergone an independent mathematician usability study. Mathlib and general PDE formalization are not integrated. Example lemmas test the workflow; they are not claimed as new mathematics or as complete solutions of LRC or Navier–Stokes.
Kernel acceptance, semantic interpretation, independent review and novelty are separate statuses. A failed tactic is not a counterexample. Finite search exhaustion is not a universal impossibility result. A changed hypothesis creates a new claim rather than silently replacing the original.
The runtime targets macOS/Linux with Python 3.10+ and Lean 4.33.1. Lean is installed locally when needed; no compiler or AI account is bundled. Executed environments are documented in validation receipts and GitHub Actions runs. The backend's conservative Lean filter is not a sandbox for hostile public submissions.
## Executed examples
- [Integer energy bookkeeping](examples/energy-dossier/REPORT.md): a failed first proof, a repaired proof of the same proposition, and a checked refutation after removing a sign assumption. This does not prove analytic PDE estimates.
- [A concrete LRC tuple](examples/lrc-witness/REPORT.md): a modular witness at 1/14 for thirteen speeds, with checkpoint continuation. The real-circle bridge and universal tuple coverage remain separate obligations.
## Reproduce and develop
The host AI can run these steps for the mathematician. See [operator documentation](docs/OPERATIONS.md) and the [English dossier protocol](plugins/math-research-collaborator/skills/math-research/references/dossiers.md).
```sh
python scripts/acceptance.py --workspace .math-research
```
If the pinned compiler is missing, use the bundled project-local bootstrap first. An existing compiler can be supplied with `--lean-bin /path/to/bin`.
The HTML interface has no runtime dependencies. Rebuild it with `python scripts/build_ui.py`. UI tests use `npm ci`, `npx playwright install chromium` and `npm run test:ui`. Source changes require review before regenerating the manifest; see [CONTRIBUTING.md](CONTRIBUTING.md).
## Documentation
- [English guide](docs/ENGLISH.md) and [Vietnamese mathematician guide](docs/MATHEMATICIANS.md)
- [Capabilities and acceptance](docs/CAPABILITIES.md)
- [Reference Lean core and semantic review](reference-core/README.md)
- [Research evaluation form](docs/USER_TRIAL.md)
- [Release notes](CHANGELOG.md)
- [Rights and attribution](docs/RIGHTS.md)
Maintained under [nclamvn](https://github.com/nclamvn). AI assisted the implementation, documentation and formalization. Cite the version actually used and report its verification scope. No open-source license has been selected; public availability does not imply unrestricted redistribution or relicensing.