Research collaboration
Bring a question or an idea.
For researchers, AI-for-math teams, and technical collaborators. Tell us what you work on and where it connects to KeyAI.
Start a conversation on GitHubContact and collaboration
Help make the work stronger.
Review a proof, reproduce a result, or explore a research workflow with us. A short, concrete introduction is enough to start.
Review and reproducibility
Check a specific result.
Point to a theorem, assumption, experiment, or source. A minimal reproduction and the source commit help us investigate.
Open a research reviewResearch OS pilot
Test one repeated workflow.
For Lean and formal-methods teams that lose context between research sessions. Help us understand the problem and test the current workspace.
Apply for the workflow pilotThe workflow pilot
One session. A concrete next decision.
Plan for 60 minutes: a brief fit and scope check, orientation in the public workspace, a walkthrough of a repeated research problem, and a decision about a possible next test.
Bring a public or sanitized example, your current verifier, and one place where your workflow loses evidence or context.
- Current status
- Recruiting
- Completed external pilots
- 0
This is a research pilot. A hosted multi-project product is not yet available; external adoption and product fit remain unvalidated.
Read the full session and evaluation protocolBefore you contact us
GitHub issues are public.
Share only public or sanitized information. Do not include keys, credentials, personal records, confidential repositories, or unpublished sensitive material.
For a sensitive finding, first ask for a private channel without including the details.
Any cryptographic instance must be synthetic, a published challenge, or owned and explicitly authorized by the participant. The pilot does not accept requests involving live funds, accounts, third-party assets, or key recovery.
Read the research and publication boundaries →Full pilot protocol and evaluation criteria
Who the pilot is for
Technical lead of an AI-for-mathematics or formalization team
- Technical lead of an AI-for-mathematics or formalization team
- Formal-methods researcher reviewing AI-generated artifacts
- Maintainer of a multi-week Lean project with human and AI contributors
Fit signals
- The team has a real, repeated workflow involving claims, evidence, tasks, and verifier results.
- At least two people or agents contribute across more than one session.
- The participant can provide a public or sanitized summary for qualification.
- The participant can attend one observed onboarding session and make an explicit build, change, stop, or pending decision.
Outside this pilot
- Requests to solve a cryptographic key or recover a secret.
- A one-off proof request with no durable research-state problem.
- A public intake that requires secrets, credentials, private keys, internal architecture, or confidential workflow details.
- A request for a finished hosted, authenticated, multi-project product.
Session plan
Qualify
Confirm the primary user, repeated workflow, authorization basis, sanitized boundary, and decision owner.
Exit gateProceed only when the pain is repeated, the qualification summary is safe to retain, and a discovery disposition can be made.
Orient
Observe the participant using the current secp256k1 workspace without a guided tour.
Exit gateRecord whether the participant can explain current state, blocker, and next action in 10 minutes or less. Treat this as a usability diagnostic, not product-value validation.
Map workflow
Map one sanitized real workflow into ingest, structure, decide, execute, verify, and retain without executing a candidate.
Exit gateThe participant identifies a repeated failure and the smallest adapter boundary that could test it under TASK-012.
Set disposition
Choose build, change, stop, or pending and record the narrowest justified next step.
Exit gateA discovery decision is recorded without treating interest, scheduling, or orientation success as retention or MVP validation.
Evaluation criteria
No external pilot session has been completed or recorded.
| Measure | What is observed | Target | Evidence |
|---|---|---|---|
orientation-timeusability_diagnostic |
Elapsed observed time until the participant correctly states current decision, main blocker, and active next action. | 10 minutes or less | Timestamped observer notes |
repeated-painprimary |
The participant names a failure that recurs across sessions or contributors and describes its present workaround. | One specific repeated workflow with a concrete consequence | Participant wording and workflow map |
workflow-fitprimary |
A sanitized real workflow maps to the six-stage product loop and exposes a smallest adapter boundary without executing a candidate. | One bounded adapter contract or an explicit reason the loop does not fit | Sanitized workflow map and discovery disposition |
discovery-dispositionprimary |
The project lead records exactly one build, change, stop, or pending outcome under the priority rules. | One dated disposition linked to CH-001 | Participant-approved sanitized decision record |
second-sessionmvp_outcome |
The same team returns for an observed second-project session; a promise or scheduled date alone is not completion. | One completed return session under TASK-012; not required to close TASK-011 discovery | Dated TASK-012 session record |
provenance-completenessguardrail |
Every promoted pilot artifact links to source, task, decision, trust classification, and the applicable verifier or validation method. Observational evidence is labeled observational. | 100 percent | Pilot evidence record |
generator-editsmvp_diagnostic |
Number of KeyAI generator-code edits required to represent the second project. | Zero for the MVP; discover the expected boundary in TASK-011 and measure it only in TASK-012 | TASK-012 change log |
public-data-safetyguardrail |
Secrets, credentials, private keys, personal data, or confidential material placed in the public intake or evidence log. | Zero | Intake and evidence review |
Decision rules
One observed discovery session, one explicit build/change/stop/pending disposition for CH-001, and no customer or retention claim beyond the recorded behavior.
Build
- The participant demonstrates the repeated research-state pain.
- The sanitized workflow maps to the product loop and exposes a minimum adapter boundary.
- The participant authorizes a bounded TASK-012 test; no execution is performed in TASK-011.
Change
- The pain is real but the current workspace or language blocks orientation.
- The workflow maps to the product loop but requires a narrower user, verifier, or artifact contract.
- A specific product or trust-boundary change is required before an adapter test can be justified.
Stop
- The problem is a one-off proof request rather than durable research-state coordination.
- The request involves unauthorized cryptographic targets, live funds, secrets, or unsafe data handling.
- No repeated pain or workflow fit is identified.
Pending
- The participant appears relevant but the available evidence is insufficient or cannot yet be sanitized.
- A decision owner, authorization basis, or bounded workflow map is still missing.
- Pending does not unlock TASK-012 and is not evidence of retention.
Authorization and retention
The secp256k1 reference environment maps and verifies a research boundary. It does not solve the plain secp256k1 discrete logarithm problem.
- Pilot authority
- TASK-011 authorizes qualification, observation, and workflow mapping only. It does not authorize executing a new research or cryptanalytic candidate.
- Experiment gate
- A second-project execution requires TASK-012 authorization. Any secp256k1 or ECDLP experiment additionally requires a superseding route-selection decision, a selected route, and a promoted task and hypothesis with success and stop conditions.
- Evidence retention
- The repository retains only participant-approved sanitized summaries and decision evidence. Observational evidence is labeled observational and is not presented as machine verification.
Never submit
- private keys or seed phrases
- credentials or access tokens
- personal data
- confidential repositories or unpublished material without permission
- internal workflow or architecture details not approved for public disclosure
- live-funds, account-recovery, or third-party cryptographic targets
Protocol reference: TASK-011
Inspect the canonical protocol