diff --git a/README.md b/README.md index 1604f9a..8172015 100644 --- a/README.md +++ b/README.md @@ -276,6 +276,12 @@ Experiments have IDs (`P0`, `E0`-`E11`); the registry, phases, gates and convent [`docs/experiments/README.md`](docs/experiments/README.md). CI runner and environment notes: [`docs/infrastructure/runner-lean435.md`](docs/infrastructure/runner-lean435.md). +Browse the [65-item semantic simplex schema review](docs/reviews/simplex-schemas.html) +by opening that HTML file in a browser after cloning, or downloading it from Git. +It shows role schemas and Lean signature expressions; textbook passages and full assistant +judgment explanations remain private. The [schema design and replay instructions](docs/simplex-schema.md) +explain how the page is generated and which annotations still need review. + ## What this does not claim Lean says whether the code is *legal*, and — when there is a proof — whether it is @@ -285,4 +291,5 @@ well-formed statement of the wrong theorem passes every check here. `confidence` possible; spot-check before trusting a dataset. Source books are not committed. `.gitignore` keeps PDFs and extracted text out of -the repository; only code and the short Lean datasets belong in git. +the repository. The tracked schema review contains semantic annotations and Lean signatures, +while source-inclusive inputs remain in the ignored data directory. diff --git a/docs/experiments/P0-execution-2026-10-28.md b/docs/experiments/P0-execution-2026-10-28.md new file mode 100644 index 0000000..4620bc7 --- /dev/null +++ b/docs/experiments/P0-execution-2026-10-28.md @@ -0,0 +1,84 @@ +# P0 execution report: 2026-10-28 + +**Status: blocked by provider billing. No GO, PARTIAL or NO-GO decision.** +The owner requested delivery of the fixes and this report now, with the remaining paid calls deferred. + +## What ran + +The owner explicitly authorized sending the 65 textbook passages and corresponding Lean code +through the existing DashScope endpoint to `qwen-max`, at temperature 0 and a cumulative ceiling +of 400 HTTP requests. The run issued **131 HTTP requests**. Provider responses accounted for +**37,699 input tokens and 7,790 output tokens**, 45,489 total. These are recorded token counts, +not an invoice or a monetary cost estimate. The client counted 89 received model responses; +a received response is not necessarily a usable detector result. + +| Coverage | Count | +|---|---:| +| Original cohort | 65 | +| Items with both detectors complete | 42 | +| Items with one or both detectors missing | 23 | +| Successful role-extraction/alignment components | 45 | +| Successful judge components | 43 | +| Missing role components | 20 | +| Missing judge components | 22 | +| Remaining request reservations | 269 | + +DashScope returned HTTP 400 with error code `Arrearage` and its overdue-payment reference. +The first runner implementation recorded the failures and continued through the cohort, so +65 saved rows did not mean 65 successful items. The scorer rejected these incomplete outputs. +No partial-sample gate decision or performance comparison has been produced. + +## Inputs and labels + +The default `items.jsonl` export omitted `source_text`. All 65 original passages were recovered +from the matching detection spans and checked byte-for-byte against the archived private +`review.json`. Item IDs and Lean code were unchanged. The recovery tool also verifies every +exported field against the archive, normalizing the archive's JSON-encoded imports field. +Source-inclusive inputs and the regenerated labeling HTML remain in the ignored data directory. + +The owner replaced the planned Kimi/human labeling with Codex annotation. All 65 labels were +frozen before the first detector request. They contain 30 faithful, 25 wrong, 7 minor drift and +3 not-formalizable verdicts. This is one AI annotator, **not human gold**. The annotator saw the +detector implementation and aggregate compilation counts, but not per-item compiler outcomes +or detector outputs. Syntax/proof defects were ignored when the intended semantics were recoverable; +no compiler or API-name audit was performed. Independent human auditing remains necessary before +using these labels as evidence for paper-level claims. + +## Execution repairs + +- Empty passages and mismatched frozen inputs/labels are rejected before paid calls. +- Each HTTP attempt reserves cumulative budget before sending, including transport and JSON retries. + Model, endpoint, temperature, input/label/prompt hashes and cumulative token usage are persisted. +- Billing/authentication errors now stop immediately, preserving partial results. +- Resume keeps every successful detector component and retries only missing components. Existing + rows are replaced atomically rather than duplicated. A budget stop also preserves completed work + within the current item. A lock prevents concurrent writers. +- `--audit-only` reconciles saved metadata without API calls. It confirmed 42 complete items, + 23 incomplete items, 42 missing components and 131 already-consumed request reservations. +- Scoring requires complete results and unchanged frozen-label/result hashes. It restores the + preregistered complementary-signal PARTIAL rule and uses wrong versus faithful for primary metrics; + minor drift is included as positive only in the secondary comparison. +- Detector prompts, matching thresholds, the concept table and frozen annotations were not tuned + against these outputs. Recovery changes concern transport, persistence and accounting only. + +The private first-attempt output and metadata were backed up before reconciliation. The results +hash and the frozen-label hash did not change during the offline audit. + +## Validation and next action + +149 offline unit tests passed, including billing-stop and partial-resume regressions; repository-wide +Ruff and diff checks passed. These checks did not compile Lean or build Docker locally. +The initial PR revision passed Python tests and real Lean validation on +`ubuntu24.04-x64-lean4.35`, runner 7, in [CI #427](https://gitea.entroia.com/Zayden-Jung/lean-bench/actions/runs/427). +The image job was skipped by the PR workflow. The recovery revision passed [CI #433](https://gitea.entroia.com/Zayden-Jung/lean-bench/actions/runs/433). +The recovery changes from PR #6 are consolidated with the semantic schema and review page +in PR #9; the combined head is checked separately there. + +After the owner confirms billing recovery, resume the existing run with the same inputs, frozen +labels and cumulative budget. There are 42 missing components; retries may consume more requests. +Do not change model or prompts to work around the provider block. Only after all 65 items have +successful outputs should the scorer produce the registered decision and disagreement report. +Phase 1 has not started. + +Tracked audit data: `experiments/P0-pilot/results/execution.json` (counts and hashes only). +Private raw files: `experiments/P0-pilot/data/` (gitignored). diff --git a/docs/experiments/P0-pilot.md b/docs/experiments/P0-pilot.md index efc2b90..6414444 100644 --- a/docs/experiments/P0-pilot.md +++ b/docs/experiments/P0-pilot.md @@ -2,7 +2,11 @@ Experiment ID **P0**, Phase 0. Registry and conventions: [README.md](README.md). -Status: **approved 2026-10-22; 65 AI labels frozen 2026-10-28; detector execution pending explicit data-transfer approval. No pilot API request has been sent.** +Status: **approved 2026-10-22; 65 AI labels frozen 2026-10-28; detector run blocked by DashScope Arrearage after 131 requests. 42 items are complete, 23 need missing detector components. No gate decision has been issued.** + +The owner explicitly authorized sending the 65 passages and Lean code to DashScope/qwen-max, +then requested fixes and an execution report now, with paid recovery calls deferred. +Execution report: [P0 execution, 2026-10-28](P0-execution-2026-10-28.md). Owner amendment (2026-10-28, in the execution chat): Codex now handles preparation, annotation, detector execution and reporting; Kimi's participation is no longer required. diff --git a/docs/research-plan.md b/docs/research-plan.md index 0b163c3..b444060 100644 --- a/docs/research-plan.md +++ b/docs/research-plan.md @@ -8,9 +8,15 @@ Evidence base: repo README and code (`leanbench/`, 4,345 lines incl. tests), pro ## 0. The idea in one page +**Terminology clarification (2026-10-28).** The owner uses "simplex" for a semantic, +multi-role relation schema: one statement joins objects, assumptions and a conclusion. +It does not mean a geometric simplex or assert a mathematical simplicial complex. +See [the implemented schema design](simplex-schema.md) for scoped slots, storage and +candidate retrieval. Existing signature projections and AI source annotations remain partial. + **Simplex, as it exists in the archived code.** - `Role(name, context, choices)`: a named semantic slot with a description and an optional closed set of allowed values (`is_constrained`, `validate_value`). -- `Simplex(name, roles: {alias: Role})`: a reusable unit of **at least two** roles. A Simplex is itself a `Role`, so simplices nest; nesting gives a *simplicial complex*. `Equivalence` is the two-role special case. +- `Simplex(name, roles: {alias: Role})`: a reusable unit of **at least two** roles. A Simplex is itself a `Role`, so explicitly supplied schemas can be nested as semantic composition. `Equivalence` is the two-role special case. - `State` / `Fact` / `Goal`: a role plus a value. A `Fact` has a value, a `Goal` does not; `SolvingTask.is_completed()` is "every goal resolved". - `SchemaRegistry` (SQLite): `set_role`, `set_simplex`, `search_roles`, `find_by_roles(known_roles)`, `find_solvable(known_role_names)`. - `SchemaParserAgent`: turns a query into a Simplex through a forced tool call whose JSON schema says `minItems: 2`, with a **search-first, reuse-before-create** rule for roles. `AnalogySchemaMiner`: proposes new simplices by the ratio *Simplex B : Role B :: Simplex A : Role A*. @@ -19,11 +25,11 @@ Evidence base: repo README and code (`leanbench/`, 4,345 lines incl. tests), pro | Lean | Simplex view | |---|---| -| `(G : Type*) [Group G]` | role `G`, `context` = "carrier", `choices` = admissible type/class constraints | +| `(G : Type*) [Group G]` | role `G`, `context` = "carrier", type/class constraints as attributes; `choices` only for explicit finite value sets | | `(h : P x)` hypothesis | `Fact` role | | conclusion after the final `:` | `Goal` role | | `def` / `structure` being introduced | `own` role (what the thing *is*) | -| a lemma used inside a proof | nested simplex (edge in the complex) | +| a lemma used inside a proof | explicit nested schema reference (when recorded) | `leanbench/typeindex.py` already extracts exactly this split: `input` (binders and hypotheses), `goal` (the conclusion), `own` (definitions). So the type index is a simplex index in all but name. The new work is to make it a **first-class schema that steers inference** instead of a passive index. diff --git a/docs/reviews/simplex-schemas.html b/docs/reviews/simplex-schemas.html new file mode 100644 index 0000000..298ae8b --- /dev/null +++ b/docs/reviews/simplex-schemas.html @@ -0,0 +1,9341 @@ +
Schema annotation seeds, not independently validated mathematical statements. A simplex joins the objects, assumptions and conclusion in its slots. References are partial symbol/syntax candidates. This review contains schema annotations and Lean signature text, not textbook passages or full assistant judgment explanations.
{
+ "name": "schema:p0-f12735802ba0:548ab1a767a685aefa146455:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "object1",
+ "kind": "object",
+ "context": "field",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "field"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "fact1",
+ "kind": "fact",
+ "context": "commutative ring",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "commutative",
+ "ring"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact2": {
+ "name": "fact2",
+ "kind": "fact",
+ "context": "identity nonzero",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "identity",
+ "nonzero"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "nonzero elements are units",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "nonzero",
+ "elements",
+ "are",
+ "units"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:548ab1a767a685aefa146455:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "F": {
+ "name": "F",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "own": {
+ "name": "own",
+ "kind": "own",
+ "type": "class",
+ "attrs": {
+ "keyword": "class",
+ "references": [],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:6ea85a17cb5decb0670c4afe:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "whole group",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "whole",
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "object3",
+ "kind": "object",
+ "context": "identity singleton",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "identity",
+ "singleton"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "both sets are subgroups",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "both",
+ "sets",
+ "are",
+ "subgroups"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:6ea85a17cb5decb0670c4afe:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "Subgroup G (Set.univ : Set G) ∧ Subgroup G {1}",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:389a27cbae1957943fae2960:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "object1",
+ "kind": "object",
+ "context": "integer ring",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "integer",
+ "ring"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "unit",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "unit"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "units equal plus minus one",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "units",
+ "equal",
+ "plus",
+ "minus",
+ "one"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:389a27cbae1957943fae2960:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "premise1": {
+ "name": "premise1",
+ "kind": "fact",
+ "type": "(u : ℤ)",
+ "attrs": {
+ "binder_kind": "goal_implication",
+ "classified_by": "implication",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "premise2": {
+ "name": "premise2",
+ "kind": "fact",
+ "type": "IsUnit u",
+ "attrs": {
+ "binder_kind": "goal_implication",
+ "classified_by": "implication",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "u = 1 ∨ u = -1",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:b63f0ed4d1ea1e11e34e6f8a:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "a",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "a"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "generated subgroup equals integer powers",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "generated",
+ "subgroup",
+ "equals",
+ "integer",
+ "powers"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:b63f0ed4d1ea1e11e34e6f8a:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "implicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "a": {
+ "name": "a",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "\\<a\\> = {a ^ k | k : ℤ}",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "a"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:db4553333550bccbd3f0e21d:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": true,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "H",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "H"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "φ",
+ "kind": "object",
+ "context": "map between groups",
+ "attrs": {
+ "symbols": [
+ "φ"
+ ],
+ "keywords": [
+ "map",
+ "between",
+ "groups"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "φ",
+ "kind": "fact",
+ "context": "bijective",
+ "attrs": {
+ "symbols": [
+ "φ"
+ ],
+ "keywords": [
+ "bijective"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object3"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact2": {
+ "name": "φ",
+ "kind": "fact",
+ "context": "preserves multiplication",
+ "attrs": {
+ "symbols": [
+ "φ"
+ ],
+ "keywords": [
+ "preserves",
+ "multiplication"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object3"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "isomorphic iff such map exists",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "isomorphic",
+ "iff",
+ "such",
+ "map",
+ "exists"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:db4553333550bccbd3f0e21d:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "H": {
+ "name": "H",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group H"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "own": {
+ "name": "own",
+ "kind": "own",
+ "type": "Prop",
+ "attrs": {
+ "keyword": "def",
+ "references": [],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:c3e75089fbfe8f386b4a22ec:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "a",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "a"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "b",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "b"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "inverse product reverses inverse factors",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "inverse",
+ "product",
+ "reverses",
+ "inverse",
+ "factors"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:c3e75089fbfe8f386b4a22ec:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "implicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "a": {
+ "name": "a",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "b": {
+ "name": "b",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "(a * b)⁻¹ = b⁻¹ * a⁻¹",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "a",
+ "b"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:91a6a0c1c21014bf08ffa3b6:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": true,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "n",
+ "kind": "object",
+ "context": "integer modulus",
+ "attrs": {
+ "symbols": [
+ "n"
+ ],
+ "keywords": [
+ "integer",
+ "modulus"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "p",
+ "kind": "object",
+ "context": "prime factor",
+ "attrs": {
+ "symbols": [
+ "p"
+ ],
+ "keywords": [
+ "prime",
+ "factor"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "q",
+ "kind": "object",
+ "context": "prime factor",
+ "attrs": {
+ "symbols": [
+ "q"
+ ],
+ "keywords": [
+ "prime",
+ "factor"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object4": {
+ "name": "φ",
+ "kind": "object",
+ "context": "totient function",
+ "attrs": {
+ "symbols": [
+ "φ"
+ ],
+ "keywords": [
+ "totient",
+ "function"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "φ",
+ "kind": "fact",
+ "context": "totient value can be found",
+ "attrs": {
+ "symbols": [
+ "φ"
+ ],
+ "keywords": [
+ "totient",
+ "value",
+ "can",
+ "be",
+ "found"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object4"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "recover both prime factors",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "recover",
+ "both",
+ "prime",
+ "factors"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:91a6a0c1c21014bf08ffa3b6:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "n": {
+ "name": "n",
+ "kind": "object",
+ "type": "ℕ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "p": {
+ "name": "p",
+ "kind": "object",
+ "type": "ℕ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "q": {
+ "name": "q",
+ "kind": "object",
+ "type": "ℕ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "hn": {
+ "name": "hn",
+ "kind": "fact",
+ "type": "n = p * q",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "n",
+ "p",
+ "q"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "hpq": {
+ "name": "hpq",
+ "kind": "fact",
+ "type": "p.Prime ∧ q.Prime",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "p",
+ "q"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "premise1": {
+ "name": "premise1",
+ "kind": "fact",
+ "type": "∃ (φ : ℕ → ℕ), (∀ m, φ m = Nat.totient m)",
+ "attrs": {
+ "binder_kind": "goal_implication",
+ "classified_by": "implication",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "∃ (p' q' : ℕ), n = p' * q' ∧ p'.Prime ∧ q'.Prime",
+ "attrs": {
+ "exists_count": 1,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "n"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:675ac9dbf3ec8a0553149a96:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "H",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "H"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "φ",
+ "kind": "object",
+ "context": "isomorphism",
+ "attrs": {
+ "symbols": [
+ "φ"
+ ],
+ "keywords": [
+ "isomorphism"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object4": {
+ "name": "g",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "g"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "φ",
+ "kind": "fact",
+ "context": "group isomorphism",
+ "attrs": {
+ "symbols": [
+ "φ"
+ ],
+ "keywords": [
+ "group",
+ "isomorphism"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object3"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "map preserves identity and inverses",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "map",
+ "preserves",
+ "identity",
+ "and",
+ "inverses"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:675ac9dbf3ec8a0553149a96:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "implicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "H": {
+ "name": "H",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "implicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group H"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "φ (1 : G) = (1 : H) ∧ ∀ g : G, φ g⁻¹ = (φ g)⁻¹",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 1,
+ "is_iff": false,
+ "references": [
+ "G",
+ "H"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:8b39fc5b656bac00bc1e863f:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "object1",
+ "kind": "object",
+ "context": "cyclic group",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "cyclic",
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "rectangle symmetry group",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "rectangle",
+ "symmetry",
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object4": {
+ "name": "H",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "H"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object5": {
+ "name": "φ",
+ "kind": "object",
+ "context": "isomorphism",
+ "attrs": {
+ "symbols": [
+ "φ"
+ ],
+ "keywords": [
+ "isomorphism"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object6": {
+ "name": "g",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "g"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object7": {
+ "name": "n",
+ "kind": "object",
+ "context": "natural number",
+ "attrs": {
+ "symbols": [
+ "n"
+ ],
+ "keywords": [
+ "natural",
+ "number"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "nonisomorphism and preservation of powers",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "nonisomorphism",
+ "and",
+ "preservation",
+ "of",
+ "powers"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}Insufficient projected roles; no object roles were invented.
{
+ "name": "schema:p0-f12735802ba0:3549ad65eee67f7b432a8b70:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": true,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "a",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "a"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "b",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "b"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "left right equations uniquely solvable",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "left",
+ "right",
+ "equations",
+ "uniquely",
+ "solvable"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:3549ad65eee67f7b432a8b70:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "implicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "a": {
+ "name": "a",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "b": {
+ "name": "b",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "\\\\(∃! x : G, a * x = b) ∧ (∃! x : G, x * a = b)",
+ "attrs": {
+ "exists_count": 2,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "G",
+ "a",
+ "b"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:0b7db1a8100c33a50a08981f:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "n",
+ "kind": "object",
+ "context": "group size",
+ "attrs": {
+ "symbols": [
+ "n"
+ ],
+ "keywords": [
+ "group",
+ "size"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "g",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "g"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "G",
+ "kind": "fact",
+ "context": "finite",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "finite"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object1"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "nth power equals identity",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "nth",
+ "power",
+ "equals",
+ "identity"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:0b7db1a8100c33a50a08981f:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G",
+ "Fintype G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "g": {
+ "name": "g",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "g ^ Fintype.card G = 1",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "G",
+ "g"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:e3d40d93cda13ec59c35d9a5:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": true,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "object1",
+ "kind": "object",
+ "context": "RSA method",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "rsa",
+ "method"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "messages",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "messages"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "design secure authenticated message exchange",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "design",
+ "secure",
+ "authenticated",
+ "message",
+ "exchange"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}Insufficient projected roles; no object roles were invented.
{
+ "name": "schema:p0-f12735802ba0:aaf1250a5104a4f7c1ca0d29:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "n",
+ "kind": "object",
+ "context": "modulus",
+ "attrs": {
+ "symbols": [
+ "n"
+ ],
+ "keywords": [
+ "modulus"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "a",
+ "kind": "object",
+ "context": "integer",
+ "attrs": {
+ "symbols": [
+ "a"
+ ],
+ "keywords": [
+ "integer"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "Φ",
+ "kind": "object",
+ "context": "group of units",
+ "attrs": {
+ "symbols": [
+ "Φ"
+ ],
+ "keywords": [
+ "group",
+ "of",
+ "units"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "a",
+ "kind": "fact",
+ "context": "relatively prime to modulus",
+ "attrs": {
+ "symbols": [
+ "a"
+ ],
+ "keywords": [
+ "relatively",
+ "prime",
+ "to",
+ "modulus"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object2"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "totient power congruent to one",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "totient",
+ "power",
+ "congruent",
+ "to",
+ "one"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:aaf1250a5104a4f7c1ca0d29:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "n": {
+ "name": "n",
+ "kind": "object",
+ "type": "ℕ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "a": {
+ "name": "a",
+ "kind": "object",
+ "type": "ℤ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "h": {
+ "name": "h",
+ "kind": "fact",
+ "type": "Nat.Coprime a n",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "predicate",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "a",
+ "n"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "(a ^ Nat.totient n) ≡ 1 [ZMOD n]",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "a",
+ "n"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:57966f39253aba58777a4ffd:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "X",
+ "kind": "object",
+ "context": "set",
+ "attrs": {
+ "symbols": [
+ "X"
+ ],
+ "keywords": [
+ "set"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "real valued functions",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "real",
+ "valued",
+ "functions"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "ring identity and unit characterization",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "ring",
+ "identity",
+ "and",
+ "unit",
+ "characterization"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:57966f39253aba58777a4ffd:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "X": {
+ "name": "X",
+ "kind": "object",
+ "type": "Type",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "Ring (X → ℝ)",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "X"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:6ef921c49672c73f8f3e0edf:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": true,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "G",
+ "kind": "fact",
+ "context": "finite",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "finite"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object1"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "rows columns contain elements once",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "rows",
+ "columns",
+ "contain",
+ "elements",
+ "once"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:6ef921c49672c73f8f3e0edf:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G",
+ "Fintype G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "g": {
+ "name": "g",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "h": {
+ "name": "h",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "\\\\\\n ∃! (x : G), x * g = h \\\\\\n ∧ ∃! (y : G), g * y = h",
+ "attrs": {
+ "exists_count": 2,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "G",
+ "g",
+ "h"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:371fe1b32fe04da354ad4478:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "H",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "H"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "K",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "K"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object4": {
+ "name": "object4",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "H",
+ "kind": "fact",
+ "context": "finite",
+ "attrs": {
+ "symbols": [
+ "H"
+ ],
+ "keywords": [
+ "finite"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object2"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact2": {
+ "name": "K",
+ "kind": "fact",
+ "context": "finite",
+ "attrs": {
+ "symbols": [
+ "K"
+ ],
+ "keywords": [
+ "finite"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object3"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact3": {
+ "name": "G",
+ "kind": "fact",
+ "context": "isomorphic to product",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "isomorphic",
+ "to",
+ "product"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object1"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "element order divides lcm sizes",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "element",
+ "order",
+ "divides",
+ "lcm",
+ "sizes"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:371fe1b32fe04da354ad4478:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "H": {
+ "name": "H",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Fintype H",
+ "Group H"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "K": {
+ "name": "K",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Fintype K",
+ "Group K"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "g": {
+ "name": "g",
+ "kind": "object",
+ "type": "H × K",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "H",
+ "K"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "OrderOf g ∣ lcm (Fintype.card H) (Fintype.card K)",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "H",
+ "K",
+ "g"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:a7396b1a5d5ebcd5b48ea7ba:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "object1",
+ "kind": "object",
+ "context": "real numbers",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "real",
+ "numbers"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "rational numbers",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "rational",
+ "numbers"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "object3",
+ "kind": "object",
+ "context": "complex numbers",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "complex",
+ "numbers"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object4": {
+ "name": "object4",
+ "kind": "object",
+ "context": "integers",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "integers"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object5": {
+ "name": "object5",
+ "kind": "object",
+ "context": "real polynomial ring",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "real",
+ "polynomial",
+ "ring"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "three fields two nonfields",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "three",
+ "fields",
+ "two",
+ "nonfields"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}Insufficient projected roles; no object roles were invented.
{
+ "name": "schema:p0-f12735802ba0:59bb865c9bdfb8521e414743:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "object1",
+ "kind": "object",
+ "context": "complex numbers",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "complex",
+ "numbers"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "norm one subset",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "norm",
+ "one",
+ "subset"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "object3",
+ "kind": "object",
+ "context": "nonzero complex numbers",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "nonzero",
+ "complex",
+ "numbers"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "unit modulus set is subgroup",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "unit",
+ "modulus",
+ "set",
+ "is",
+ "subgroup"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}Insufficient projected roles; no object roles were invented.
{
+ "name": "schema:p0-f12735802ba0:283d407566264b02fbee6560:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "a",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "a"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "generated cyclic subgroup",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "generated",
+ "cyclic",
+ "subgroup"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "element order defined by subgroup size",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "element",
+ "order",
+ "defined",
+ "by",
+ "subgroup"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:283d407566264b02fbee6560:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "a": {
+ "name": "a",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "own": {
+ "name": "own",
+ "kind": "own",
+ "type": "ℕ",
+ "attrs": {
+ "keyword": "def",
+ "references": [],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:7de228e675b949cd64850c04:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "e",
+ "kind": "object",
+ "context": "identity element",
+ "attrs": {
+ "symbols": [
+ "e"
+ ],
+ "keywords": [
+ "identity",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "e'",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "e'"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object4": {
+ "name": "g",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "g"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "fact1",
+ "kind": "fact",
+ "context": "left product equals g",
+ "attrs": {
+ "symbols": [
+ "e'",
+ "g"
+ ],
+ "keywords": [
+ "left",
+ "product",
+ "equals",
+ "g"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object3",
+ "object4"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "element equals group identity",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "element",
+ "equals",
+ "group",
+ "identity"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:7de228e675b949cd64850c04:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "e'": {
+ "name": "e'",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "g": {
+ "name": "g",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "h": {
+ "name": "h",
+ "kind": "fact",
+ "type": "e' * g = g",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "e'",
+ "g"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "e' = 1",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "e'"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:dc1c450987f3e3a5285260f7:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "H",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "H"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "φ",
+ "kind": "object",
+ "context": "isomorphism",
+ "attrs": {
+ "symbols": [
+ "φ"
+ ],
+ "keywords": [
+ "isomorphism"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "φ",
+ "kind": "fact",
+ "context": "group isomorphism",
+ "attrs": {
+ "symbols": [
+ "φ"
+ ],
+ "keywords": [
+ "group",
+ "isomorphism"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object3"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "abelian iff target abelian",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "abelian",
+ "iff",
+ "target",
+ "abelian"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:dc1c450987f3e3a5285260f7:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "implicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "H": {
+ "name": "H",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "implicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group H"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "\\\\\\n Commutative (*) ↔ Commutative ((*) : H → H → H)",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": true,
+ "references": [
+ "H"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:c42dc687ecc042f5b7a00a9d:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": true,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "object1",
+ "kind": "object",
+ "context": "finite group",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "finite",
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "fact1",
+ "kind": "fact",
+ "context": "finite",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "finite"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "each row column permutes group",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "each",
+ "row",
+ "column",
+ "permutes",
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:c42dc687ecc042f5b7a00a9d:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Fintype G",
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "\\/\\n (∀ g : G, ∀ g' : G, ∃! h : G, g * h = g') ∧ \\/\\n (∀ g : G, ∀ g' : G, ∃! h : G, h * g = g')",
+ "attrs": {
+ "exists_count": 2,
+ "forall_count": 4,
+ "is_iff": false,
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:8491370b02906b6efdb3da5e:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "n",
+ "kind": "object",
+ "context": "natural modulus",
+ "attrs": {
+ "symbols": [
+ "n"
+ ],
+ "keywords": [
+ "natural",
+ "modulus"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "p",
+ "kind": "object",
+ "context": "prime",
+ "attrs": {
+ "symbols": [
+ "p"
+ ],
+ "keywords": [
+ "prime"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "q",
+ "kind": "object",
+ "context": "prime",
+ "attrs": {
+ "symbols": [
+ "q"
+ ],
+ "keywords": [
+ "prime"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object4": {
+ "name": "m",
+ "kind": "object",
+ "context": "integer exponent",
+ "attrs": {
+ "symbols": [
+ "m"
+ ],
+ "keywords": [
+ "integer",
+ "exponent"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object5": {
+ "name": "a",
+ "kind": "object",
+ "context": "integer",
+ "attrs": {
+ "symbols": [
+ "a"
+ ],
+ "keywords": [
+ "integer"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "n",
+ "kind": "fact",
+ "context": "product of primes",
+ "attrs": {
+ "symbols": [
+ "n"
+ ],
+ "keywords": [
+ "product",
+ "of",
+ "primes"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object1"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact2": {
+ "name": "m",
+ "kind": "fact",
+ "context": "lcm predecessors",
+ "attrs": {
+ "symbols": [
+ "m"
+ ],
+ "keywords": [
+ "lcm",
+ "predecessors"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object4"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact3": {
+ "name": "a",
+ "kind": "fact",
+ "context": "relatively prime to modulus",
+ "attrs": {
+ "symbols": [
+ "a"
+ ],
+ "keywords": [
+ "relatively",
+ "prime",
+ "to",
+ "modulus"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object5"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "exponent power congruent to one",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "exponent",
+ "power",
+ "congruent",
+ "to",
+ "one"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:8491370b02906b6efdb3da5e:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "p": {
+ "name": "p",
+ "kind": "object",
+ "type": "ℕ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "q": {
+ "name": "q",
+ "kind": "object",
+ "type": "ℕ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "hp": {
+ "name": "hp",
+ "kind": "fact",
+ "type": "Nat.Prime p",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "predicate",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "p"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "hq": {
+ "name": "hq",
+ "kind": "fact",
+ "type": "Nat.Prime q",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "predicate",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "q"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "n": {
+ "name": "n",
+ "kind": "object",
+ "type": "ℕ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "hn": {
+ "name": "hn",
+ "kind": "fact",
+ "type": "n = p * q",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "n",
+ "p",
+ "q"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "m": {
+ "name": "m",
+ "kind": "object",
+ "type": "ℕ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "hm": {
+ "name": "hm",
+ "kind": "fact",
+ "type": "m = Nat.lcm (p - 1) (q - 1)",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "m",
+ "p",
+ "q"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "a": {
+ "name": "a",
+ "kind": "object",
+ "type": "ℕ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "ha": {
+ "name": "ha",
+ "kind": "fact",
+ "type": "Nat.Coprime a n",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "predicate",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "a",
+ "n"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "a ^ m ≡ 1 [ZMOD n]",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "a",
+ "m",
+ "n"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:437d02fe69d580bde075648c:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": true,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "object1",
+ "kind": "object",
+ "context": "painted square",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "painted",
+ "square"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "color preserving symmetries",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "color",
+ "preserving",
+ "symmetries"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "identify symmetry group size isomorphism",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "identify",
+ "symmetry",
+ "group",
+ "size",
+ "isomorphism"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}Insufficient projected roles; no object roles were invented.
{
+ "name": "schema:p0-f12735802ba0:5fe4f3fbbead7e6988f015a9:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "a",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "a"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "x",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "x"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object4": {
+ "name": "y",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "y"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "left and right cancellation implications",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "left",
+ "and",
+ "right",
+ "cancellation",
+ "implications"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:5fe4f3fbbead7e6988f015a9:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "implicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "a": {
+ "name": "a",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "x": {
+ "name": "x",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "y": {
+ "name": "y",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "premise1": {
+ "name": "premise1",
+ "kind": "fact",
+ "type": "a * x = a * y",
+ "attrs": {
+ "binder_kind": "goal_implication",
+ "classified_by": "implication",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "a",
+ "x",
+ "y"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "x = y",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "x",
+ "y"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:8a55f59982e50e4af47b3d55:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "a",
+ "kind": "object",
+ "context": "integer",
+ "attrs": {
+ "symbols": [
+ "a"
+ ],
+ "keywords": [
+ "integer"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "h",
+ "kind": "object",
+ "context": "integer",
+ "attrs": {
+ "symbols": [
+ "h"
+ ],
+ "keywords": [
+ "integer"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "m",
+ "kind": "object",
+ "context": "exponent modulus",
+ "attrs": {
+ "symbols": [
+ "m"
+ ],
+ "keywords": [
+ "exponent",
+ "modulus"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object4": {
+ "name": "n",
+ "kind": "object",
+ "context": "modulus",
+ "attrs": {
+ "symbols": [
+ "n"
+ ],
+ "keywords": [
+ "modulus"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "h",
+ "kind": "fact",
+ "context": "congruent one modulo m",
+ "attrs": {
+ "symbols": [
+ "h"
+ ],
+ "keywords": [
+ "congruent",
+ "one",
+ "modulo",
+ "m"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object2"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "power congruent to original integer",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "power",
+ "congruent",
+ "to",
+ "original",
+ "integer"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:8a55f59982e50e4af47b3d55:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "a": {
+ "name": "a",
+ "kind": "object",
+ "type": "ℤ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "h": {
+ "name": "h",
+ "kind": "object",
+ "type": "ℤ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "m": {
+ "name": "m",
+ "kind": "object",
+ "type": "ℤ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "n": {
+ "name": "n",
+ "kind": "object",
+ "type": "ℤ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "hn": {
+ "name": "hn",
+ "kind": "fact",
+ "type": "h % m = 1",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "h",
+ "m"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "hm": {
+ "name": "hm",
+ "kind": "fact",
+ "type": "m ∣ n",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "m",
+ "n"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "a ^ h ≡ a [ZMOD n]",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "a",
+ "h",
+ "n"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:8d4d64143a8b214e38d7ba1b:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "S_4",
+ "kind": "object",
+ "context": "permutation group",
+ "attrs": {
+ "symbols": [
+ "S_4"
+ ],
+ "keywords": [
+ "permutation",
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "π",
+ "kind": "object",
+ "context": "permutation",
+ "attrs": {
+ "symbols": [
+ "π"
+ ],
+ "keywords": [
+ "permutation"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "object3",
+ "kind": "object",
+ "context": "stabilizer subgroup",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "stabilizer",
+ "subgroup"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "π",
+ "kind": "fact",
+ "context": "fixes fourth point",
+ "attrs": {
+ "symbols": [
+ "π"
+ ],
+ "keywords": [
+ "fixes",
+ "fourth",
+ "point"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object2"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "stabilizer subgroup isomorphic to S3",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "stabilizer",
+ "subgroup",
+ "isomorphic",
+ "to",
+ "s"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}Insufficient projected roles; no object roles were invented.
{
+ "name": "schema:p0-f12735802ba0:6017927fdafd91ca22ed6ade:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "a",
+ "kind": "object",
+ "context": "rational number",
+ "attrs": {
+ "symbols": [
+ "a"
+ ],
+ "keywords": [
+ "rational",
+ "number"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "b",
+ "kind": "object",
+ "context": "rational number",
+ "attrs": {
+ "symbols": [
+ "b"
+ ],
+ "keywords": [
+ "rational",
+ "number"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "object3",
+ "kind": "object",
+ "context": "real quadratic subset",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "real",
+ "quadratic",
+ "subset"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object4": {
+ "name": "object4",
+ "kind": "object",
+ "context": "conjugation map",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "conjugation",
+ "map"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "subset field conjugation is automorphism",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "subset",
+ "field",
+ "conjugation",
+ "is",
+ "automorphism"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}Insufficient projected roles; no object roles were invented.
{
+ "name": "schema:p0-f12735802ba0:089c452ec2f9b850733a44f6:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "H",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "H"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "φ",
+ "kind": "object",
+ "context": "isomorphism",
+ "attrs": {
+ "symbols": [
+ "φ"
+ ],
+ "keywords": [
+ "isomorphism"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object4": {
+ "name": "g",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "g"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object5": {
+ "name": "n",
+ "kind": "object",
+ "context": "natural number",
+ "attrs": {
+ "symbols": [
+ "n"
+ ],
+ "keywords": [
+ "natural",
+ "number"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "φ",
+ "kind": "fact",
+ "context": "group isomorphism",
+ "attrs": {
+ "symbols": [
+ "φ"
+ ],
+ "keywords": [
+ "group",
+ "isomorphism"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object3"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "map preserves powers and identity powers",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "map",
+ "preserves",
+ "powers",
+ "and",
+ "identity"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:089c452ec2f9b850733a44f6:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "implicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "H": {
+ "name": "H",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "implicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group H"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "g": {
+ "name": "g",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "n": {
+ "name": "n",
+ "kind": "object",
+ "type": "ℕ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "\\/\\/ φ(g^n) = (φ g)^n ∧ (g^n = 1 → (φ g)^n = 1)",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "g",
+ "n"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:75009c3d616f02be4d7a5824:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "M",
+ "kind": "object",
+ "context": "set",
+ "attrs": {
+ "symbols": [
+ "M"
+ ],
+ "keywords": [
+ "set"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "N",
+ "kind": "object",
+ "context": "subset",
+ "attrs": {
+ "symbols": [
+ "N"
+ ],
+ "keywords": [
+ "subset"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "n",
+ "kind": "object",
+ "context": "integer",
+ "attrs": {
+ "symbols": [
+ "n"
+ ],
+ "keywords": [
+ "integer"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object4": {
+ "name": "a",
+ "kind": "object",
+ "context": "sequence of elements",
+ "attrs": {
+ "symbols": [
+ "a"
+ ],
+ "keywords": [
+ "sequence",
+ "of",
+ "elements"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "M",
+ "kind": "fact",
+ "context": "associative operation",
+ "attrs": {
+ "symbols": [
+ "M"
+ ],
+ "keywords": [
+ "associative",
+ "operation"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object1"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact2": {
+ "name": "N",
+ "kind": "fact",
+ "context": "closed under multiplication",
+ "attrs": {
+ "symbols": [
+ "N"
+ ],
+ "keywords": [
+ "closed",
+ "under",
+ "multiplication"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object2"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact3": {
+ "name": "n",
+ "kind": "fact",
+ "context": "positive",
+ "attrs": {
+ "symbols": [
+ "n"
+ ],
+ "keywords": [
+ "positive"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object3"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact4": {
+ "name": "a",
+ "kind": "fact",
+ "context": "elements belong to subset",
+ "attrs": {
+ "symbols": [
+ "a"
+ ],
+ "keywords": [
+ "elements",
+ "belong",
+ "to",
+ "subset"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object4"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "ordered product belongs to subset",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "ordered",
+ "product",
+ "belongs",
+ "to",
+ "subset"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:75009c3d616f02be4d7a5824:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "M": {
+ "name": "M",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "implicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Semigroup M"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "N": {
+ "name": "N",
+ "kind": "object",
+ "type": "Set M",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "M"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "hN": {
+ "name": "hN",
+ "kind": "fact",
+ "type": "∀ x y ∈ N, x * y ∈ N",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "N"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "n": {
+ "name": "n",
+ "kind": "object",
+ "type": "ℕ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "hn": {
+ "name": "hn",
+ "kind": "fact",
+ "type": "1 ≤ n",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "n"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "a": {
+ "name": "a",
+ "kind": "object",
+ "type": "Fin n → M",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "M",
+ "n"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "ha": {
+ "name": "ha",
+ "kind": "fact",
+ "type": "∀ i, a i ∈ N",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "N",
+ "a"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "(∏ i, a i) ∈ N",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "N",
+ "a"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:9091f6a277215174e821d373:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "φ",
+ "kind": "object",
+ "context": "previously defined ring map",
+ "attrs": {
+ "symbols": [
+ "φ"
+ ],
+ "keywords": [
+ "previously",
+ "defined",
+ "ring",
+ "map"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "verify this map preserves ring operations",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "verify",
+ "this",
+ "map",
+ "preserves",
+ "ring"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:9091f6a277215174e821d373:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "R": {
+ "name": "R",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Ring R"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "S": {
+ "name": "S",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Ring S"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "IsRingHom φ",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:0cd2f0368a0d8234c2593845:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": true,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "n",
+ "kind": "object",
+ "context": "matrix size",
+ "attrs": {
+ "symbols": [
+ "n"
+ ],
+ "keywords": [
+ "matrix",
+ "size"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "T",
+ "kind": "object",
+ "context": "real matrix",
+ "attrs": {
+ "symbols": [
+ "T"
+ ],
+ "keywords": [
+ "real",
+ "matrix"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "evaluation at matrix is homomorphism",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "evaluation",
+ "at",
+ "matrix",
+ "is",
+ "homomorphism"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:0cd2f0368a0d8234c2593845:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "n": {
+ "name": "n",
+ "kind": "object",
+ "type": "ℕ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "T": {
+ "name": "T",
+ "kind": "object",
+ "type": "Matrix n n ℝ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "n"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "RingHom (Polynomial ℝ) (Matrix n n ℝ)",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "n"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:8e55e625fa9b10b7b65f59f4:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": true,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "G",
+ "kind": "fact",
+ "context": "four elements",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "four",
+ "elements"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object1"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "nonidentity element squares to identity",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "nonidentity",
+ "element",
+ "squares",
+ "to",
+ "identity"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:8e55e625fa9b10b7b65f59f4:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "hG": {
+ "name": "hG",
+ "kind": "fact",
+ "type": "Fintype.card G = 4",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "∃ g : G, g ≠ 1 ∧ g * g = 1",
+ "attrs": {
+ "exists_count": 1,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:534c6ffcf56931559e70657b:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "S_3",
+ "kind": "object",
+ "context": "symmetric group",
+ "attrs": {
+ "symbols": [
+ "S_3"
+ ],
+ "keywords": [
+ "symmetric",
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "cyclic group",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "cyclic",
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "nonabelian and abelian hence nonisomorphic",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "nonabelian",
+ "and",
+ "abelian",
+ "hence",
+ "nonisomorphic"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}Insufficient projected roles; no object roles were invented.
{
+ "name": "schema:p0-f12735802ba0:aa16561dceee591e35e42c4d:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": true,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "M",
+ "kind": "object",
+ "context": "set",
+ "attrs": {
+ "symbols": [
+ "M"
+ ],
+ "keywords": [
+ "set"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "n",
+ "kind": "object",
+ "context": "integer",
+ "attrs": {
+ "symbols": [
+ "n"
+ ],
+ "keywords": [
+ "integer"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "M",
+ "kind": "fact",
+ "context": "associative operation",
+ "attrs": {
+ "symbols": [
+ "M"
+ ],
+ "keywords": [
+ "associative",
+ "operation"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object1"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact2": {
+ "name": "n",
+ "kind": "fact",
+ "context": "positive",
+ "attrs": {
+ "symbols": [
+ "n"
+ ],
+ "keywords": [
+ "positive"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object2"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "unique coherent associative product family",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "unique",
+ "coherent",
+ "associative",
+ "product",
+ "family"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:aa16561dceee591e35e42c4d:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "M": {
+ "name": "M",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Semigroup M"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "n": {
+ "name": "n",
+ "kind": "object",
+ "type": "ℕ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "h": {
+ "name": "h",
+ "kind": "fact",
+ "type": "n ≥ 1",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "n"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "premise1": {
+ "name": "premise1",
+ "kind": "fact",
+ "type": "∃! f : (Fin n → M)",
+ "attrs": {
+ "binder_kind": "goal_implication",
+ "classified_by": "implication",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "M",
+ "n"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "M, (∀ a : M, f ![a] = a) ∧ (∀ a b : M, f ![a, b] = a * b) ∧ (∀ (k : ℕ) (hk : 1 ≤ k) (hnk : k < n) (a : Fin n → M), f a = f (a ↾ k) * f (a ∘ (Fin.succAbove k).symm))",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 3,
+ "is_iff": false,
+ "references": [
+ "M",
+ "n"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:73ec95bfac2896218d2b1dab:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "C_n",
+ "kind": "object",
+ "context": "root of unity group",
+ "attrs": {
+ "symbols": [
+ "C_n"
+ ],
+ "keywords": [
+ "root",
+ "of",
+ "unity",
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "n",
+ "kind": "object",
+ "context": "order",
+ "attrs": {
+ "symbols": [
+ "n"
+ ],
+ "keywords": [
+ "order"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "ξ",
+ "kind": "object",
+ "context": "complex exponential generator",
+ "attrs": {
+ "symbols": [
+ "ξ"
+ ],
+ "keywords": [
+ "complex",
+ "exponential",
+ "generator"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "cyclic with specified order generator",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "cyclic",
+ "with",
+ "specified",
+ "order",
+ "generator"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:73ec95bfac2896218d2b1dab:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "n": {
+ "name": "n",
+ "kind": "object",
+ "type": "ℕ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "h": {
+ "name": "h",
+ "kind": "fact",
+ "type": "n > 0",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "n"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "IsCyclic (ZMod n)",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "n"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:6b5a55ec3bb3c85239919649:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "C_n",
+ "kind": "object",
+ "context": "root of unity set",
+ "attrs": {
+ "symbols": [
+ "C_n"
+ ],
+ "keywords": [
+ "root",
+ "of",
+ "unity",
+ "set"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "n",
+ "kind": "object",
+ "context": "integer",
+ "attrs": {
+ "symbols": [
+ "n"
+ ],
+ "keywords": [
+ "integer"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "k",
+ "kind": "object",
+ "context": "integer",
+ "attrs": {
+ "symbols": [
+ "k"
+ ],
+ "keywords": [
+ "integer"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "k",
+ "kind": "fact",
+ "context": "between zero and n minus one",
+ "attrs": {
+ "symbols": [
+ "k"
+ ],
+ "keywords": [
+ "between",
+ "zero",
+ "and",
+ "n",
+ "minus"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object3"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "roots equal specified exponential set",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "roots",
+ "equal",
+ "specified",
+ "exponential",
+ "set"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:6b5a55ec3bb3c85239919649:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "n": {
+ "name": "n",
+ "kind": "object",
+ "type": "ℕ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "own": {
+ "name": "own",
+ "kind": "own",
+ "type": "Subgroup ℂ",
+ "attrs": {
+ "keyword": "def",
+ "references": [],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:d6ddc1df3ce6b764f3fb8d73:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "H",
+ "kind": "object",
+ "context": "subset",
+ "attrs": {
+ "symbols": [
+ "H"
+ ],
+ "keywords": [
+ "subset"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "H",
+ "kind": "fact",
+ "context": "nonempty",
+ "attrs": {
+ "symbols": [
+ "H"
+ ],
+ "keywords": [
+ "nonempty"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object2"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact2": {
+ "name": "H",
+ "kind": "fact",
+ "context": "closed under products",
+ "attrs": {
+ "symbols": [
+ "H"
+ ],
+ "keywords": [
+ "closed",
+ "under",
+ "products"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object2"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact3": {
+ "name": "H",
+ "kind": "fact",
+ "context": "closed under inverses",
+ "attrs": {
+ "symbols": [
+ "H"
+ ],
+ "keywords": [
+ "closed",
+ "under",
+ "inverses"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object2"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "conditions imply subgroup and identity",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "conditions",
+ "imply",
+ "subgroup",
+ "and",
+ "identity"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:d6ddc1df3ce6b764f3fb8d73:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "implicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "H": {
+ "name": "H",
+ "kind": "object",
+ "type": "Set G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "h_one": {
+ "name": "h_one",
+ "kind": "fact",
+ "type": "∀ h ∈ H, h⁻¹ ∈ H",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "H"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "h_mul": {
+ "name": "h_mul",
+ "kind": "fact",
+ "type": "∀ h1 h2 ∈ H, h1 * h2 ∈ H",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "H"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "IsSubgroup H",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "H"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:ed87589326312890bea42d7c:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "K",
+ "kind": "object",
+ "context": "field",
+ "attrs": {
+ "symbols": [
+ "K"
+ ],
+ "keywords": [
+ "field"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "Laurent polynomials",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "laurent",
+ "polynomials"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "ring with identity and units",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "ring",
+ "with",
+ "identity",
+ "and",
+ "units"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:ed87589326312890bea42d7c:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "K": {
+ "name": "K",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Field K"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "Ring (LaurentSeries K)",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "K"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:d609c5bb746fc0e05625134a:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "f",
+ "kind": "object",
+ "context": "map",
+ "attrs": {
+ "symbols": [
+ "f"
+ ],
+ "keywords": [
+ "map"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "n",
+ "kind": "object",
+ "context": "modulus",
+ "attrs": {
+ "symbols": [
+ "n"
+ ],
+ "keywords": [
+ "modulus"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "object3",
+ "kind": "object",
+ "context": "integers",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "integers"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object4": {
+ "name": "object4",
+ "kind": "object",
+ "context": "residue ring",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "residue",
+ "ring"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "canonical residue map is homomorphism",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "canonical",
+ "residue",
+ "map",
+ "is",
+ "homomorphism"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:d609c5bb746fc0e05625134a:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "n": {
+ "name": "n",
+ "kind": "object",
+ "type": "ℕ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "RingHom ℤ (ZMod n)",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "n"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:4405f31187373d5e1de622d2:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "n",
+ "kind": "object",
+ "context": "natural number",
+ "attrs": {
+ "symbols": [
+ "n"
+ ],
+ "keywords": [
+ "natural",
+ "number"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "S_n",
+ "kind": "object",
+ "context": "symmetric group",
+ "attrs": {
+ "symbols": [
+ "S_n"
+ ],
+ "keywords": [
+ "symmetric",
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "factorial cardinality always nonabelian when n≥3",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "factorial",
+ "cardinality",
+ "always",
+ "nonabelian",
+ "when"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:4405f31187373d5e1de622d2:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "n": {
+ "name": "n",
+ "kind": "object",
+ "type": "ℕ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "hn": {
+ "name": "hn",
+ "kind": "fact",
+ "type": "n ≥ 3",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "n"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "\\n Fintype.card (Symmetric n) = n! ∧ ¬ IsAbelian (Symmetric n)",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "n"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:05a6defa23576b7da41f8fbf:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "H",
+ "kind": "object",
+ "context": "subset",
+ "attrs": {
+ "symbols": [
+ "H"
+ ],
+ "keywords": [
+ "subset"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "H",
+ "kind": "fact",
+ "context": "nonempty",
+ "attrs": {
+ "symbols": [
+ "H"
+ ],
+ "keywords": [
+ "nonempty"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object2"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact2": {
+ "name": "H",
+ "kind": "fact",
+ "context": "subgroup",
+ "attrs": {
+ "symbols": [
+ "H"
+ ],
+ "keywords": [
+ "subgroup"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object2"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "product closure is necessary",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "product",
+ "closure",
+ "is",
+ "necessary"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:05a6defa23576b7da41f8fbf:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "implicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "H": {
+ "name": "H",
+ "kind": "object",
+ "type": "Set G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "h_nonempty": {
+ "name": "h_nonempty",
+ "kind": "object",
+ "type": "H.Nonempty",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "H"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "h_prod": {
+ "name": "h_prod",
+ "kind": "fact",
+ "type": "∀ h1 h2 ∈ H, h1 * h2 ∈ H",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "H"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "IsSubgroup H",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "H"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:47c39e88c29e3974e8864e90:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": true,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "object1",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "fact1",
+ "kind": "fact",
+ "context": "order two",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "order",
+ "two"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "unique group up to isomorphism",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "unique",
+ "group",
+ "up",
+ "to",
+ "isomorphism"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:47c39e88c29e3974e8864e90:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G",
+ "Fintype G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "H": {
+ "name": "H",
+ "kind": "object",
+ "type": "Type",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group H",
+ "Fintype H"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "hG": {
+ "name": "hG",
+ "kind": "fact",
+ "type": "Fintype.card G = 2",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "hH": {
+ "name": "hH",
+ "kind": "fact",
+ "type": "Fintype.card H = 2",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "H"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "Nonempty (G ≃* H)",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "G",
+ "H"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:fa61f8cb0e88b11e158c4eec:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "a",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "a"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "b",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "b"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "abelian defined by commuting products",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "abelian",
+ "defined",
+ "by",
+ "commuting",
+ "products"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:fa61f8cb0e88b11e158c4eec:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "own": {
+ "name": "own",
+ "kind": "own",
+ "type": "Prop",
+ "attrs": {
+ "keyword": "class",
+ "references": [],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:3c00c37b39285cbd7d0be732:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": true,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "object1",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "fact1",
+ "kind": "fact",
+ "context": "order three",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "order",
+ "three"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "unique group up to isomorphism",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "unique",
+ "group",
+ "up",
+ "to",
+ "isomorphism"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}Insufficient projected roles; no object roles were invented.
{
+ "name": "schema:p0-f12735802ba0:186d922a4121917ac8643316:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "object1",
+ "kind": "object",
+ "context": "real three variable polynomials",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "real",
+ "three",
+ "variable",
+ "polynomials"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "ring identity and unit characterization",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "ring",
+ "identity",
+ "and",
+ "unit",
+ "characterization"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}Insufficient projected roles; no object roles were invented.
{
+ "name": "schema:p0-f12735802ba0:e845a95d7b5054a0dbdf34eb:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "d",
+ "kind": "object",
+ "context": "integer",
+ "attrs": {
+ "symbols": [
+ "d"
+ ],
+ "keywords": [
+ "integer"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "generated subgroup",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "generated",
+ "subgroup"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "integer multiples cyclic opposite generators equal",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "integer",
+ "multiples",
+ "cyclic",
+ "opposite",
+ "generators"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:e845a95d7b5054a0dbdf34eb:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "d": {
+ "name": "d",
+ "kind": "object",
+ "type": "ℤ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "(Submodule.span ℤ {d}) = {n * d | n : ℤ}",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "d"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:e7a3cec23c2ecdc655dd12cf:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "h",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "h"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "g",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "g"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "fact1",
+ "kind": "fact",
+ "context": "product equals identity",
+ "attrs": {
+ "symbols": [
+ "h",
+ "g"
+ ],
+ "keywords": [
+ "product",
+ "equals",
+ "identity"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object2",
+ "object3"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "left inverse equals inverse element",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "left",
+ "inverse",
+ "equals",
+ "inverse",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:e7a3cec23c2ecdc655dd12cf:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "implicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "h": {
+ "name": "h",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "g": {
+ "name": "g",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "hg": {
+ "name": "hg",
+ "kind": "fact",
+ "type": "h * g = 1",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "g",
+ "h"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "h = g⁻¹",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "g",
+ "h"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:e966f3b17e32318acd5f2762:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "g",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "g"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "inverse of inverse equals element",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "inverse",
+ "of",
+ "inverse",
+ "equals",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:e966f3b17e32318acd5f2762:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "implicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "g": {
+ "name": "g",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "g = (g⁻¹)⁻¹",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "g"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:2c420bf6ec32069ecd0043dc:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "R",
+ "kind": "object",
+ "context": "set",
+ "attrs": {
+ "symbols": [
+ "R"
+ ],
+ "keywords": [
+ "set"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "addition",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "addition"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "object3",
+ "kind": "object",
+ "context": "multiplication",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "multiplication"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "R",
+ "kind": "fact",
+ "context": "nonempty",
+ "attrs": {
+ "symbols": [
+ "R"
+ ],
+ "keywords": [
+ "nonempty"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object1"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "ring defined by additive group associativity distributivity",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "ring",
+ "defined",
+ "by",
+ "additive",
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:2c420bf6ec32069ecd0043dc:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "R": {
+ "name": "R",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "own": {
+ "name": "own",
+ "kind": "own",
+ "type": "structure",
+ "attrs": {
+ "keyword": "structure",
+ "references": [],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:25af34567cb2040bf41869e5:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "C_4",
+ "kind": "object",
+ "context": "fourth roots",
+ "attrs": {
+ "symbols": [
+ "C_4"
+ ],
+ "keywords": [
+ "fourth",
+ "roots"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "complex multiplication",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "complex",
+ "multiplication"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "specified roots form group with identity",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "specified",
+ "roots",
+ "form",
+ "group",
+ "with"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}Insufficient projected roles; no object roles were invented.
{
+ "name": "schema:p0-f12735802ba0:578ae89f353ecbdc0ffb76a2:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "K",
+ "kind": "object",
+ "context": "field",
+ "attrs": {
+ "symbols": [
+ "K"
+ ],
+ "keywords": [
+ "field"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "polynomials over field",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "polynomials",
+ "over",
+ "field"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "commutative ring identity units constant",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "commutative",
+ "ring",
+ "identity",
+ "units",
+ "constant"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:578ae89f353ecbdc0ffb76a2:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "K": {
+ "name": "K",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Field K"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "\\\\[isCommutativeRing (Polynomial K) ∧ (1 : Polynomial K) = 1 ∧ ∀ p : Polynomial K, IsUnit p → ∃ a : K, p = C a := by \\\\- sorry",
+ "attrs": {
+ "exists_count": 1,
+ "forall_count": 1,
+ "is_iff": false,
+ "references": [
+ "K"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:1a8d6a5c9aa3cc5000dee474:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "group order is cardinality",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "group",
+ "order",
+ "is",
+ "cardinality"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:1a8d6a5c9aa3cc5000dee474:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G",
+ "Fintype G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "own": {
+ "name": "own",
+ "kind": "own",
+ "type": "ℕ",
+ "attrs": {
+ "keyword": "def",
+ "references": [],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:450c7df89ecd284b0e08504a:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "n",
+ "kind": "object",
+ "context": "modulus",
+ "attrs": {
+ "symbols": [
+ "n"
+ ],
+ "keywords": [
+ "modulus"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "d",
+ "kind": "object",
+ "context": "residue",
+ "attrs": {
+ "symbols": [
+ "d"
+ ],
+ "keywords": [
+ "residue"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "object3",
+ "kind": "object",
+ "context": "generated cyclic subgroup",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "generated",
+ "cyclic",
+ "subgroup"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "subgroup equals integer and residue multiples",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "subgroup",
+ "equals",
+ "integer",
+ "and",
+ "residue"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:450c7df89ecd284b0e08504a:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "n": {
+ "name": "n",
+ "kind": "object",
+ "type": "ℕ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "d": {
+ "name": "d",
+ "kind": "object",
+ "type": "ℕ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "hn": {
+ "name": "hn",
+ "kind": "fact",
+ "type": "0 < n",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "n"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "\\\\\\n (ZMod n).subgroup.closure ({ZMod.mk d} : Set (ZMod n)) = \\\\\\n {ZMod.mk (k * d % n) | k : ℤ} = \\\\\\n {ZMod.mk (k * d % n) | k : ZMod n}",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "d",
+ "n"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:f908ac15b1bf8228281bcf68:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "object1",
+ "kind": "object",
+ "context": "first group",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "first",
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "second group",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "second",
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "fact1",
+ "kind": "fact",
+ "context": "groups are isomorphic",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "groups",
+ "are",
+ "isomorphic"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "abelian properties equivalent",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "abelian",
+ "properties",
+ "equivalent"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:f908ac15b1bf8228281bcf68:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "H": {
+ "name": "H",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group H"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "iso": {
+ "name": "iso",
+ "kind": "fact",
+ "type": "G ≃* H",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G",
+ "H"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "(IsAbelian G ↔ IsAbelian H)",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": true,
+ "references": [
+ "G",
+ "H"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:bcdfa01447e7060e1fd3d935:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": true,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "object1",
+ "kind": "object",
+ "context": "RSA method",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "rsa",
+ "method"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "message",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "message"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "design message authentication method",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "design",
+ "message",
+ "authentication",
+ "method"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}Insufficient projected roles; no object roles were invented.
{
+ "name": "schema:p0-f12735802ba0:f86421f93f1381d2ce728bc1:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "R",
+ "kind": "object",
+ "context": "ring",
+ "attrs": {
+ "symbols": [
+ "R"
+ ],
+ "keywords": [
+ "ring"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "S",
+ "kind": "object",
+ "context": "ring",
+ "attrs": {
+ "symbols": [
+ "S"
+ ],
+ "keywords": [
+ "ring"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "f",
+ "kind": "object",
+ "context": "map",
+ "attrs": {
+ "symbols": [
+ "f"
+ ],
+ "keywords": [
+ "map"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object4": {
+ "name": "a",
+ "kind": "object",
+ "context": "ring element",
+ "attrs": {
+ "symbols": [
+ "a"
+ ],
+ "keywords": [
+ "ring",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object5": {
+ "name": "b",
+ "kind": "object",
+ "context": "ring element",
+ "attrs": {
+ "symbols": [
+ "b"
+ ],
+ "keywords": [
+ "ring",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "homomorphism preserves operations bijective means isomorphism",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "homomorphism",
+ "preserves",
+ "operations",
+ "bijective",
+ "means"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:f86421f93f1381d2ce728bc1:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "R": {
+ "name": "R",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "implicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Ring R"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "S": {
+ "name": "S",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "implicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Ring S"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "f": {
+ "name": "f",
+ "kind": "object",
+ "type": "R → S",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "R",
+ "S"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "Function.IsRingHom f ↔ (∀ a b : R, f (a + b) = f a + f b ∧ f (a * b) = f a * f b)",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 1,
+ "is_iff": true,
+ "references": [
+ "R",
+ "f"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:89fe687db9136379cd276fff:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": true,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "object1",
+ "kind": "object",
+ "context": "cyclic group",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "cyclic",
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "rectangle symmetry group",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "rectangle",
+ "symmetry",
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "nonisomorphic groups of order four",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "nonisomorphic",
+ "groups",
+ "of",
+ "order",
+ "four"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}Insufficient projected roles; no object roles were invented.
{
+ "name": "schema:p0-f12735802ba0:da65aa56505f6c13e6553d0d:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "H",
+ "kind": "object",
+ "context": "subset",
+ "attrs": {
+ "symbols": [
+ "H"
+ ],
+ "keywords": [
+ "subset"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "H",
+ "kind": "fact",
+ "context": "nonempty",
+ "attrs": {
+ "symbols": [
+ "H"
+ ],
+ "keywords": [
+ "nonempty"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object2"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "subgroup iff group under inherited operation",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "subgroup",
+ "iff",
+ "group",
+ "under",
+ "inherited"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:da65aa56505f6c13e6553d0d:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "H": {
+ "name": "H",
+ "kind": "object",
+ "type": "Set G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "h_nonempty": {
+ "name": "h_nonempty",
+ "kind": "object",
+ "type": "H.Nonempty",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "H"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "Subgroup.of G H ↔ IsGroup (H, (*), 1, ⁻¹)",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": true,
+ "references": [
+ "G",
+ "H"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:ab2990e9786d5bda5a04e067:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "T",
+ "kind": "object",
+ "context": "map",
+ "attrs": {
+ "symbols": [
+ "T"
+ ],
+ "keywords": [
+ "map"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "three dimensional space",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "three",
+ "dimensional",
+ "space"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "T",
+ "kind": "fact",
+ "context": "bijective",
+ "attrs": {
+ "symbols": [
+ "T"
+ ],
+ "keywords": [
+ "bijective"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object1"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact2": {
+ "name": "T",
+ "kind": "fact",
+ "context": "continuous first partial derivatives",
+ "attrs": {
+ "symbols": [
+ "T"
+ ],
+ "keywords": [
+ "continuous",
+ "first",
+ "partial",
+ "derivatives"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object1"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "diffeomorphisms form group under composition",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "diffeomorphisms",
+ "form",
+ "group",
+ "under",
+ "composition"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:ab2990e9786d5bda5a04e067:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "U": {
+ "name": "U",
+ "kind": "object",
+ "type": "Set (ℝ × ℝ × ℝ)",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "hU": {
+ "name": "hU",
+ "kind": "fact",
+ "type": "IsOpen U",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "predicate",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "U"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "\\\\\\n Group (Subtype (fun T : (ℝ × ℝ × ℝ) → (ℝ × ℝ × ℝ) => \\\\\\n Bijective T ∧ DifferentiableOn ℝ T U ∧ ContinuousOn (fun x => deriv (T ∘ (Prod.fst, Prod.snd, Prod.third)) x) U))",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "U"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:a892779bfcaca35b91e7d611:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "T",
+ "kind": "object",
+ "context": "map",
+ "attrs": {
+ "symbols": [
+ "T"
+ ],
+ "keywords": [
+ "map"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "three dimensional space",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "three",
+ "dimensional",
+ "space"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "T",
+ "kind": "fact",
+ "context": "bijective",
+ "attrs": {
+ "symbols": [
+ "T"
+ ],
+ "keywords": [
+ "bijective"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object1"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact2": {
+ "name": "T",
+ "kind": "fact",
+ "context": "continuous",
+ "attrs": {
+ "symbols": [
+ "T"
+ ],
+ "keywords": [
+ "continuous"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object1"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact3": {
+ "name": "T",
+ "kind": "fact",
+ "context": "inverse continuous",
+ "attrs": {
+ "symbols": [
+ "T"
+ ],
+ "keywords": [
+ "inverse",
+ "continuous"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object1"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "homeomorphisms form group under composition",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "homeomorphisms",
+ "form",
+ "group",
+ "under",
+ "composition"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}Insufficient projected roles; no object roles were invented.
{
+ "name": "schema:p0-f12735802ba0:7593062cab7c74cdecec08d0:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "a",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "a"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "a",
+ "kind": "fact",
+ "context": "finite order",
+ "attrs": {
+ "symbols": [
+ "a"
+ ],
+ "keywords": [
+ "finite",
+ "order"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object1"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "least positive exponent bounded powers generate",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "least",
+ "positive",
+ "exponent",
+ "bounded",
+ "powers"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:7593062cab7c74cdecec08d0:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "a": {
+ "name": "a",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "ha": {
+ "name": "ha",
+ "kind": "fact",
+ "type": "IsOfFinOrder a",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "predicate",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "a"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "\\/\\/ (orderOf a = (min {n : ℕ | n > 0 ∧ a ^ n = 1})) ∧ (Subgroup.closure ({a} : Set G) = {a ^ k | k : ℕ, k < orderOf a})",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "G",
+ "a"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:c8204e9d19a6dd5d730dccc7:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "G",
+ "kind": "object",
+ "context": "group",
+ "attrs": {
+ "symbols": [
+ "G"
+ ],
+ "keywords": [
+ "group"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "e",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "e"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "e'",
+ "kind": "object",
+ "context": "group element",
+ "attrs": {
+ "symbols": [
+ "e'"
+ ],
+ "keywords": [
+ "group",
+ "element"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "e",
+ "kind": "fact",
+ "context": "two sided identity",
+ "attrs": {
+ "symbols": [
+ "e"
+ ],
+ "keywords": [
+ "two",
+ "sided",
+ "identity"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object2"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact2": {
+ "name": "e'",
+ "kind": "fact",
+ "context": "two sided identity",
+ "attrs": {
+ "symbols": [
+ "e'"
+ ],
+ "keywords": [
+ "two",
+ "sided",
+ "identity"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object3"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "two identities equal",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "two",
+ "identities",
+ "equal"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:c8204e9d19a6dd5d730dccc7:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "G": {
+ "name": "G",
+ "kind": "object",
+ "type": "Type*",
+ "attrs": {
+ "binder_kind": "implicit",
+ "classified_by": "sort",
+ "origin": "deterministic_signature_projection",
+ "instances": [
+ "Group G"
+ ],
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "e": {
+ "name": "e",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "e'": {
+ "name": "e'",
+ "kind": "object",
+ "type": "G",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "h_e": {
+ "name": "h_e",
+ "kind": "fact",
+ "type": "∀ g : G, e * g = g ∧ g * e = g",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G",
+ "e"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "h_e'": {
+ "name": "h_e'",
+ "kind": "fact",
+ "type": "∀ g : G, e' * g = g ∧ g * e' = g",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "G",
+ "e'"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "e = e'",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "e",
+ "e'"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:b40279b634fffd0841ff0f5a:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": false,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "a",
+ "kind": "object",
+ "context": "integer",
+ "attrs": {
+ "symbols": [
+ "a"
+ ],
+ "keywords": [
+ "integer"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "b",
+ "kind": "object",
+ "context": "integer",
+ "attrs": {
+ "symbols": [
+ "b"
+ ],
+ "keywords": [
+ "integer"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object3": {
+ "name": "r",
+ "kind": "object",
+ "context": "exponent",
+ "attrs": {
+ "symbols": [
+ "r"
+ ],
+ "keywords": [
+ "exponent"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object4": {
+ "name": "s",
+ "kind": "object",
+ "context": "exponent",
+ "attrs": {
+ "symbols": [
+ "s"
+ ],
+ "keywords": [
+ "exponent"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object5": {
+ "name": "n",
+ "kind": "object",
+ "context": "modulus",
+ "attrs": {
+ "symbols": [
+ "n"
+ ],
+ "keywords": [
+ "modulus"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "fact1": {
+ "name": "b",
+ "kind": "fact",
+ "context": "congruent to power modulo n",
+ "attrs": {
+ "symbols": [
+ "b"
+ ],
+ "keywords": [
+ "congruent",
+ "to",
+ "power",
+ "modulo",
+ "n"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [
+ "object2"
+ ],
+ "reference_status": "explicit_symbol_candidates",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "ciphertext power returns original residue",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "ciphertext",
+ "power",
+ "returns",
+ "original",
+ "residue"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:b40279b634fffd0841ff0f5a:lean:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "lean",
+ "reference_completeness": "syntactic_only"
+ },
+ "roles": {
+ "a": {
+ "name": "a",
+ "kind": "object",
+ "type": "ℤ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "b": {
+ "name": "b",
+ "kind": "object",
+ "type": "ℤ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "r": {
+ "name": "r",
+ "kind": "object",
+ "type": "ℤ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "s": {
+ "name": "s",
+ "kind": "object",
+ "type": "ℤ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "n": {
+ "name": "n",
+ "kind": "object",
+ "type": "ℤ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "t": {
+ "name": "t",
+ "kind": "object",
+ "type": "ℤ",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "default",
+ "origin": "deterministic_signature_projection",
+ "references": [],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "h1": {
+ "name": "h1",
+ "kind": "fact",
+ "type": "b ≡ a^r [ZMOD n]",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "a",
+ "b",
+ "n",
+ "r"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "h2": {
+ "name": "h2",
+ "kind": "fact",
+ "type": "r * s = 1 + n * t",
+ "attrs": {
+ "binder_kind": "explicit",
+ "classified_by": "relation",
+ "origin": "deterministic_signature_projection",
+ "references": [
+ "n",
+ "r",
+ "s",
+ "t"
+ ],
+ "reference_status": "syntactic_candidates"
+ }
+ },
+ "goal": {
+ "name": "goal",
+ "kind": "goal",
+ "type": "b^s ≡ a [ZMOD n]",
+ "attrs": {
+ "exists_count": 0,
+ "forall_count": 0,
+ "is_iff": false,
+ "references": [
+ "a",
+ "b",
+ "n",
+ "s"
+ ],
+ "reference_status": "syntactic_candidates",
+ "origin": "deterministic_signature_projection"
+ }
+ }
+ }
+}{
+ "name": "schema:p0-f12735802ba0:f8d2e206681972927560be2c:source:v1",
+ "kind": "simplex",
+ "attrs": {
+ "side": "source",
+ "goal_has_exists": true,
+ "reference_completeness": "partial"
+ },
+ "roles": {
+ "object1": {
+ "name": "object1",
+ "kind": "object",
+ "context": "nonsquare rhombus",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "nonsquare",
+ "rhombus"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "object2": {
+ "name": "object2",
+ "kind": "object",
+ "context": "geometric symmetries",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "geometric",
+ "symmetries"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ },
+ "goal1": {
+ "name": "goal1",
+ "kind": "goal",
+ "context": "identify symmetry group size and classification",
+ "attrs": {
+ "symbols": [],
+ "keywords": [
+ "identify",
+ "symmetry",
+ "group",
+ "size",
+ "and"
+ ],
+ "introduced": "given",
+ "quantifier_status": "unreviewed",
+ "references": [],
+ "reference_status": "unknown",
+ "origin": "frozen_current_chat_annotation"
+ }
+ }
+ }
+}Insufficient projected roles; no object roles were invented.
{html.escape(content)}')
+ sections.append(f'Schema annotation seeds, not independently validated mathematical statements. ' + 'A simplex joins the objects, assumptions and conclusion in its slots. ' + 'References are partial symbol/syntax candidates. ' + 'This review contains schema annotations and Lean signature text, not textbook passages ' + 'or full assistant judgment explanations.
' + ''.join(sections) + '') + (args.private_out / "schemas.html").write_text(review_page, encoding="utf-8") + if args.review_page is not None: + args.review_page.parent.mkdir(parents=True, exist_ok=True) + args.review_page.write_text(review_page, encoding="utf-8") + # JSON-only reload is independently checked; it does not use pickle. + for row in snapshots: + for side in ["source", "lean"]: + if row[side] is not None: + if role_from_dict(row[side]).as_dict() != row[side]: + raise ValueError("JSON schema roundtrip failed") + summary = {"representation": "semantic_multi_role_relation_schema_v1", "items": len(items), + "source_schemas": len(index), "lean_schemas": sum(r["lean_schema"] is not None for r in index), + "lean_incomplete": sum(r["lean_schema"] is None for r in index), "registry": info, + "hashes": {"items": digest(args.items), "assessments": digest(args.assessments), + "key": digest(args.key), "builder": digest(Path(__file__)), + "schema_module": digest(Path(__file__).resolve().parents[2] / "leanbench/schema.py"), + "registry_module": digest(Path(__file__).resolve().parents[2] / "leanbench/schema_registry.py")}, + "limitations": ["Source annotations come from a non-independent current-chat diagnostic.", + "Source quantifiers are preserved as unreviewed; existing given tags are not repaired.", + "References are symbol/syntax candidates, not complete semantic dependencies.", + "No cross-theorem identity or proof dependency is inferred.", + "Fewer than two projected Lean roles is a projection limitation, not proof that objects are absent."]} + for path, value in [(args.index, index), (args.summary, summary)]: + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(json.dumps(value, indent=2, allow_nan=False) + "\n") + print(json.dumps({k: summary[k] for k in ["items", "source_schemas", "lean_schemas", "lean_incomplete", "registry"]})) + + +if __name__ == "__main__": + main() diff --git a/experiments/P0-pilot/results/execution.json b/experiments/P0-pilot/results/execution.json new file mode 100644 index 0000000..b5a810c --- /dev/null +++ b/experiments/P0-pilot/results/execution.json @@ -0,0 +1,72 @@ +{ + "experiment": "P0", + "status": "provider_blocked", + "decision": null, + "decision_withheld_reason": "Incomplete detector outputs after DashScope Arrearage; no GO/PARTIAL/NO-GO is valid.", + "cohort_size": 65, + "completed_items": 42, + "items_with_failures": 23, + "missing_components": { + "judge": 22, + "role": 20 + }, + "request_attempts": 131, + "max_calls": 400, + "remaining_request_budget": 269, + "usage": { + "calls": 89, + "prompt_tokens": 37699, + "completion_tokens": 7790 + }, + "model": "qwen-max", + "temperature": 0.0, + "items_sha256": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed", + "labels_sha256": "1552dba85e75426799151384e7e28c9a0b1072ed4c862df0876df89920d2a638", + "results_sha256": "fce402e6eab460a48bb9a8e94140bb23f305843ab46d227bbffa5100d7de69e5", + "prompt_hashes": { + "source": "382f9a7b5a0cfb2d50d525f884dc806f45adaa59bcc45e388920c4759db1546f", + "judge": "7ab92682bd71d78a212471289f0f01db39d6b68f49d44df65d7b1c9e34ebb5e2" + }, + "labels": { + "type": "single AI annotator; not human gold", + "frozen": true, + "count": 65 + }, + "affected_blind_ids": [ + "P02", + "P04", + "P09", + "P18", + "P19", + "P20", + "P21", + "P22", + "P24", + "P27", + "P29", + "P30", + "P33", + "P36", + "P37", + "P38", + "P42", + "P43", + "P45", + "P47", + "P54", + "P59", + "P62" + ], + "successful_components_preserved": 88, + "resume_policy": "After owner confirms billing recovery, retry missing components only using the same run files, frozen labels, model, prompts and cumulative 400-request ceiling.", + "owner_instruction": "2026-10-28: complete fixes and the execution report now; resume paid calls later.", + "validation": { + "offline_unit_tests": 149, + "ruff": "passed", + "remote_runner_tag": "ubuntu24.04-x64-lean4.35", + "initial_remote_ci": "https://gitea.entroia.com/Zayden-Jung/lean-bench/actions/runs/427", + "initial_remote_ci_status": "success; image job skipped for PR", + "recovery_remote_ci": "https://gitea.entroia.com/Zayden-Jung/lean-bench/actions/runs/433", + "consolidated_pull_request": "https://gitea.entroia.com/Zayden-Jung/lean-bench/pulls/9" + } +} diff --git a/experiments/P0-pilot/results/simplex-schema-index.json b/experiments/P0-pilot/results/simplex-schema-index.json new file mode 100644 index 0000000..eaf6724 --- /dev/null +++ b/experiments/P0-pilot/results/simplex-schema-index.json @@ -0,0 +1,1210 @@ +[ + { + "blind_id": "P01", + "source_schema": "schema:p0-f12735802ba0:548ab1a767a685aefa146455:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 4, + "lean_schema": "schema:p0-f12735802ba0:548ab1a767a685aefa146455:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 1, + "fact": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "own": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P02", + "source_schema": "schema:p0-f12735802ba0:6ea85a17cb5decb0670c4afe:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 4, + "lean_schema": "schema:p0-f12735802ba0:6ea85a17cb5decb0670c4afe:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P03", + "source_schema": "schema:p0-f12735802ba0:389a27cbae1957943fae2960:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:389a27cbae1957943fae2960:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "fact": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P04", + "source_schema": "schema:p0-f12735802ba0:b63f0ed4d1ea1e11e34e6f8a:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:b63f0ed4d1ea1e11e34e6f8a:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P05", + "source_schema": "schema:p0-f12735802ba0:db4553333550bccbd3f0e21d:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 6, + "lean_schema": "schema:p0-f12735802ba0:db4553333550bccbd3f0e21d:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "fact": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "own": 1 + }, + "source_slots_with_reference_candidates": 2 + }, + { + "blind_id": "P06", + "source_schema": "schema:p0-f12735802ba0:c3e75089fbfe8f386b4a22ec:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 4, + "lean_schema": "schema:p0-f12735802ba0:c3e75089fbfe8f386b4a22ec:lean:v1", + "lean_slots": 4, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P07", + "source_schema": "schema:p0-f12735802ba0:91a6a0c1c21014bf08ffa3b6:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 6, + "lean_schema": "schema:p0-f12735802ba0:91a6a0c1c21014bf08ffa3b6:lean:v1", + "lean_slots": 7, + "lean_status": "materialized", + "source_role_counts": { + "object": 4, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "fact": 3, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P08", + "source_schema": "schema:p0-f12735802ba0:675ac9dbf3ec8a0553149a96:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 6, + "lean_schema": "schema:p0-f12735802ba0:675ac9dbf3ec8a0553149a96:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 4, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P09", + "source_schema": "schema:p0-f12735802ba0:8b39fc5b656bac00bc1e863f:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 8, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 7, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P10", + "source_schema": "schema:p0-f12735802ba0:3549ad65eee67f7b432a8b70:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 4, + "lean_schema": "schema:p0-f12735802ba0:3549ad65eee67f7b432a8b70:lean:v1", + "lean_slots": 4, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P11", + "source_schema": "schema:p0-f12735802ba0:0b7db1a8100c33a50a08981f:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:0b7db1a8100c33a50a08981f:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P12", + "source_schema": "schema:p0-f12735802ba0:e3d40d93cda13ec59c35d9a5:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P13", + "source_schema": "schema:p0-f12735802ba0:aaf1250a5104a4f7c1ca0d29:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:aaf1250a5104a4f7c1ca0d29:lean:v1", + "lean_slots": 4, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P14", + "source_schema": "schema:p0-f12735802ba0:57966f39253aba58777a4ffd:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:57966f39253aba58777a4ffd:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P15", + "source_schema": "schema:p0-f12735802ba0:6ef921c49672c73f8f3e0edf:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:6ef921c49672c73f8f3e0edf:lean:v1", + "lean_slots": 4, + "lean_status": "materialized", + "source_role_counts": { + "object": 1, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P16", + "source_schema": "schema:p0-f12735802ba0:371fe1b32fe04da354ad4478:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 8, + "lean_schema": "schema:p0-f12735802ba0:371fe1b32fe04da354ad4478:lean:v1", + "lean_slots": 4, + "lean_status": "materialized", + "source_role_counts": { + "object": 4, + "fact": 3, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "goal": 1 + }, + "source_slots_with_reference_candidates": 3 + }, + { + "blind_id": "P17", + "source_schema": "schema:p0-f12735802ba0:a7396b1a5d5ebcd5b48ea7ba:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 6, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 5, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P18", + "source_schema": "schema:p0-f12735802ba0:59bb865c9bdfb8521e414743:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 4, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 3, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P19", + "source_schema": "schema:p0-f12735802ba0:283d407566264b02fbee6560:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:283d407566264b02fbee6560:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "own": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P20", + "source_schema": "schema:p0-f12735802ba0:7de228e675b949cd64850c04:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 6, + "lean_schema": "schema:p0-f12735802ba0:7de228e675b949cd64850c04:lean:v1", + "lean_slots": 5, + "lean_status": "materialized", + "source_role_counts": { + "object": 4, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P21", + "source_schema": "schema:p0-f12735802ba0:dc1c450987f3e3a5285260f7:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:dc1c450987f3e3a5285260f7:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P22", + "source_schema": "schema:p0-f12735802ba0:c42dc687ecc042f5b7a00a9d:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:c42dc687ecc042f5b7a00a9d:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 1, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P23", + "source_schema": "schema:p0-f12735802ba0:8491370b02906b6efdb3da5e:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 9, + "lean_schema": "schema:p0-f12735802ba0:8491370b02906b6efdb3da5e:lean:v1", + "lean_slots": 11, + "lean_status": "materialized", + "source_role_counts": { + "object": 5, + "fact": 3, + "goal": 1 + }, + "lean_role_counts": { + "object": 5, + "fact": 5, + "goal": 1 + }, + "source_slots_with_reference_candidates": 3 + }, + { + "blind_id": "P24", + "source_schema": "schema:p0-f12735802ba0:437d02fe69d580bde075648c:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P25", + "source_schema": "schema:p0-f12735802ba0:5fe4f3fbbead7e6988f015a9:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:5fe4f3fbbead7e6988f015a9:lean:v1", + "lean_slots": 6, + "lean_status": "materialized", + "source_role_counts": { + "object": 4, + "goal": 1 + }, + "lean_role_counts": { + "object": 4, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P26", + "source_schema": "schema:p0-f12735802ba0:8a55f59982e50e4af47b3d55:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 6, + "lean_schema": "schema:p0-f12735802ba0:8a55f59982e50e4af47b3d55:lean:v1", + "lean_slots": 7, + "lean_status": "materialized", + "source_role_counts": { + "object": 4, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 4, + "fact": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P27", + "source_schema": "schema:p0-f12735802ba0:8d4d64143a8b214e38d7ba1b:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 3, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P28", + "source_schema": "schema:p0-f12735802ba0:6017927fdafd91ca22ed6ade:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 4, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P29", + "source_schema": "schema:p0-f12735802ba0:089c452ec2f9b850733a44f6:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 7, + "lean_schema": "schema:p0-f12735802ba0:089c452ec2f9b850733a44f6:lean:v1", + "lean_slots": 5, + "lean_status": "materialized", + "source_role_counts": { + "object": 5, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 4, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P30", + "source_schema": "schema:p0-f12735802ba0:75009c3d616f02be4d7a5824:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 9, + "lean_schema": "schema:p0-f12735802ba0:75009c3d616f02be4d7a5824:lean:v1", + "lean_slots": 8, + "lean_status": "materialized", + "source_role_counts": { + "object": 4, + "fact": 4, + "goal": 1 + }, + "lean_role_counts": { + "object": 4, + "fact": 3, + "goal": 1 + }, + "source_slots_with_reference_candidates": 4 + }, + { + "blind_id": "P31", + "source_schema": "schema:p0-f12735802ba0:9091f6a277215174e821d373:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 2, + "lean_schema": "schema:p0-f12735802ba0:9091f6a277215174e821d373:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P32", + "source_schema": "schema:p0-f12735802ba0:0cd2f0368a0d8234c2593845:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:0cd2f0368a0d8234c2593845:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P33", + "source_schema": "schema:p0-f12735802ba0:8e55e625fa9b10b7b65f59f4:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:8e55e625fa9b10b7b65f59f4:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 1, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P34", + "source_schema": "schema:p0-f12735802ba0:534c6ffcf56931559e70657b:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P35", + "source_schema": "schema:p0-f12735802ba0:aa16561dceee591e35e42c4d:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:aa16561dceee591e35e42c4d:lean:v1", + "lean_slots": 5, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "fact": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "fact": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 2 + }, + { + "blind_id": "P36", + "source_schema": "schema:p0-f12735802ba0:73ec95bfac2896218d2b1dab:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 4, + "lean_schema": "schema:p0-f12735802ba0:73ec95bfac2896218d2b1dab:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P37", + "source_schema": "schema:p0-f12735802ba0:6b5a55ec3bb3c85239919649:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:6b5a55ec3bb3c85239919649:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "own": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P38", + "source_schema": "schema:p0-f12735802ba0:d6ddc1df3ce6b764f3fb8d73:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 6, + "lean_schema": "schema:p0-f12735802ba0:d6ddc1df3ce6b764f3fb8d73:lean:v1", + "lean_slots": 5, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "fact": 3, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "fact": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 3 + }, + { + "blind_id": "P39", + "source_schema": "schema:p0-f12735802ba0:ed87589326312890bea42d7c:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:ed87589326312890bea42d7c:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P40", + "source_schema": "schema:p0-f12735802ba0:d609c5bb746fc0e05625134a:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:d609c5bb746fc0e05625134a:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 4, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P41", + "source_schema": "schema:p0-f12735802ba0:4405f31187373d5e1de622d2:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:4405f31187373d5e1de622d2:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P42", + "source_schema": "schema:p0-f12735802ba0:05a6defa23576b7da41f8fbf:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:05a6defa23576b7da41f8fbf:lean:v1", + "lean_slots": 5, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "fact": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 2 + }, + { + "blind_id": "P43", + "source_schema": "schema:p0-f12735802ba0:47c39e88c29e3974e8864e90:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:47c39e88c29e3974e8864e90:lean:v1", + "lean_slots": 5, + "lean_status": "materialized", + "source_role_counts": { + "object": 1, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "fact": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P44", + "source_schema": "schema:p0-f12735802ba0:fa61f8cb0e88b11e158c4eec:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 4, + "lean_schema": "schema:p0-f12735802ba0:fa61f8cb0e88b11e158c4eec:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "own": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P45", + "source_schema": "schema:p0-f12735802ba0:3c00c37b39285cbd7d0be732:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 1, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P46", + "source_schema": "schema:p0-f12735802ba0:186d922a4121917ac8643316:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 2, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 1, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P47", + "source_schema": "schema:p0-f12735802ba0:e845a95d7b5054a0dbdf34eb:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:e845a95d7b5054a0dbdf34eb:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P48", + "source_schema": "schema:p0-f12735802ba0:e7a3cec23c2ecdc655dd12cf:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:e7a3cec23c2ecdc655dd12cf:lean:v1", + "lean_slots": 5, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P49", + "source_schema": "schema:p0-f12735802ba0:e966f3b17e32318acd5f2762:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:e966f3b17e32318acd5f2762:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P50", + "source_schema": "schema:p0-f12735802ba0:2c420bf6ec32069ecd0043dc:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:2c420bf6ec32069ecd0043dc:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "own": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P51", + "source_schema": "schema:p0-f12735802ba0:25af34567cb2040bf41869e5:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P52", + "source_schema": "schema:p0-f12735802ba0:578ae89f353ecbdc0ffb76a2:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:578ae89f353ecbdc0ffb76a2:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P53", + "source_schema": "schema:p0-f12735802ba0:1a8d6a5c9aa3cc5000dee474:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 2, + "lean_schema": "schema:p0-f12735802ba0:1a8d6a5c9aa3cc5000dee474:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "own": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P54", + "source_schema": "schema:p0-f12735802ba0:450c7df89ecd284b0e08504a:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 4, + "lean_schema": "schema:p0-f12735802ba0:450c7df89ecd284b0e08504a:lean:v1", + "lean_slots": 4, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P55", + "source_schema": "schema:p0-f12735802ba0:f908ac15b1bf8228281bcf68:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 4, + "lean_schema": "schema:p0-f12735802ba0:f908ac15b1bf8228281bcf68:lean:v1", + "lean_slots": 4, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P56", + "source_schema": "schema:p0-f12735802ba0:bcdfa01447e7060e1fd3d935:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P57", + "source_schema": "schema:p0-f12735802ba0:f86421f93f1381d2ce728bc1:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 6, + "lean_schema": "schema:p0-f12735802ba0:f86421f93f1381d2ce728bc1:lean:v1", + "lean_slots": 4, + "lean_status": "materialized", + "source_role_counts": { + "object": 5, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P58", + "source_schema": "schema:p0-f12735802ba0:89fe687db9136379cd276fff:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P59", + "source_schema": "schema:p0-f12735802ba0:da65aa56505f6c13e6553d0d:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 4, + "lean_schema": "schema:p0-f12735802ba0:da65aa56505f6c13e6553d0d:lean:v1", + "lean_slots": 4, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P60", + "source_schema": "schema:p0-f12735802ba0:ab2990e9786d5bda5a04e067:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:ab2990e9786d5bda5a04e067:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "fact": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 2 + }, + { + "blind_id": "P61", + "source_schema": "schema:p0-f12735802ba0:a892779bfcaca35b91e7d611:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 6, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 2, + "fact": 3, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 3 + }, + { + "blind_id": "P62", + "source_schema": "schema:p0-f12735802ba0:7593062cab7c74cdecec08d0:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:7593062cab7c74cdecec08d0:lean:v1", + "lean_slots": 4, + "lean_status": "materialized", + "source_role_counts": { + "object": 1, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P63", + "source_schema": "schema:p0-f12735802ba0:c8204e9d19a6dd5d730dccc7:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 6, + "lean_schema": "schema:p0-f12735802ba0:c8204e9d19a6dd5d730dccc7:lean:v1", + "lean_slots": 6, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "fact": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "fact": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 2 + }, + { + "blind_id": "P64", + "source_schema": "schema:p0-f12735802ba0:b40279b634fffd0841ff0f5a:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 7, + "lean_schema": "schema:p0-f12735802ba0:b40279b634fffd0841ff0f5a:lean:v1", + "lean_slots": 9, + "lean_status": "materialized", + "source_role_counts": { + "object": 5, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 6, + "fact": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P65", + "source_schema": "schema:p0-f12735802ba0:f8d2e206681972927560be2c:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + } +] diff --git a/experiments/P0-pilot/results/simplex-schema-summary.json b/experiments/P0-pilot/results/simplex-schema-summary.json new file mode 100644 index 0000000..8e7ac8c --- /dev/null +++ b/experiments/P0-pilot/results/simplex-schema-summary.json @@ -0,0 +1,27 @@ +{ + "representation": "semantic_multi_role_relation_schema_v1", + "items": 65, + "source_schemas": 65, + "lean_schemas": 50, + "lean_incomplete": 15, + "registry": { + "roles": 483, + "simplices": 115, + "slots": 483 + }, + "hashes": { + "items": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed", + "assessments": "f12735802ba0d4d94b776a91581a13a508eab0ce90ba8973a6c9c4e4d1390272", + "key": "f827cac92ee4e907554fadcc7c0e006ef2b829350f74e7f8b54ca11945e62836", + "builder": "7b3a982101f620c1480d95b5e483ca6186a7e9c32ce587fb132a90bfb38a01bc", + "schema_module": "958b81e89c0befeb32d24036c130f2b37bd2e881bd5b009acf873cbcdada50ae", + "registry_module": "7b434b1eb178f597d4f60591a5ab74eff0c96a40fa751cb0ba75589b52e56271" + }, + "limitations": [ + "Source annotations come from a non-independent current-chat diagnostic.", + "Source quantifiers are preserved as unreviewed; existing given tags are not repaired.", + "References are symbol/syntax candidates, not complete semantic dependencies.", + "No cross-theorem identity or proof dependency is inferred.", + "Fewer than two projected Lean roles is a projection limitation, not proof that objects are absent." + ] +} diff --git a/experiments/P0-pilot/run_pilot.py b/experiments/P0-pilot/run_pilot.py index e226470..d4a41cf 100644 --- a/experiments/P0-pilot/run_pilot.py +++ b/experiments/P0-pilot/run_pilot.py @@ -50,37 +50,64 @@ def judge(client, passage: str, lean: str) -> dict: "reason": str(reply.get("reason", ""))[:300]} -def run_item(client, item: dict) -> dict: - if not item.get("source_text", "").strip(): - raise ValueError("Missing source_text; use a private source-inclusive export") - code = item.get("lean_code") or "" - row: dict = {"id": item["id"], "compiled": bool(item.get("verified")), "errors": {}} - proj = project(code) - row["projection"] = proj.as_dict() - row["lint"] = lint(proj) - try: - src = srcsimplex.extract_source_simplex(client, item.get("source_text", ""), - item.get("label", "")) - al = align(src, proj) - row["source"] = [r.__dict__ for r in src.roles] - row["role"] = al.as_dict() - except CallBudgetExceeded: - raise - except Exception as error: # a failed extraction is data, not a crash - row["errors"]["role"] = str(error)[:300] - try: - row["judge"] = judge(client, item.get("source_text", ""), code) - except CallBudgetExceeded: - raise - except Exception as error: - row["errors"]["judge"] = str(error)[:300] - return row +def provider_blocked(error: Exception) -> bool: + text = str(error).lower() + return any(code in text for code in ("arrearage", "overdue-payment", "invalid_api_key", "http 401", "http 403")) + + +def complete_row(row: dict) -> bool: + return not row.get("errors") and "role" in row and "judge" in row + + +class ProviderBlocked(RuntimeError): + """A billing or authentication failure requires external recovery before resuming.""" + + def __init__(self, row): + super().__init__("Provider billing/authentication blocked; partial results were preserved") + self.row = row class CallBudgetExceeded(RuntimeError): """Stop before issuing a request that would exceed the cumulative budget.""" +def run_item(client, item: dict, previous: dict | None = None) -> dict: + if not item.get("source_text", "").strip(): + raise ValueError("Missing source_text; use a private source-inclusive export") + code = item.get("lean_code") or "" + row: dict = {**(previous or {}), "id": item["id"], "compiled": bool(item.get("verified"))} + row["errors"] = dict(row.get("errors", {})) + proj = project(code) + row["projection"] = proj.as_dict() + row["lint"] = lint(proj) + if "role" not in row: + try: + src = srcsimplex.extract_source_simplex(client, item["source_text"], item.get("label", "")) + al = align(src, proj) + row["source"] = [r.__dict__ for r in src.roles] + row["role"] = al.as_dict() + row["errors"].pop("role", None) + except CallBudgetExceeded as error: + error.row = row + raise + except Exception as error: + row["errors"]["role"] = str(error)[:300] + if provider_blocked(error): + raise ProviderBlocked(row) from error + if "judge" not in row: + try: + row["judge"] = judge(client, item["source_text"], code) + row["errors"].pop("judge", None) + except CallBudgetExceeded as error: + error.row = row + raise + except Exception as error: + row["errors"]["judge"] = str(error)[:300] + if provider_blocked(error): + raise ProviderBlocked(row) from error + return row + + def digest(path: Path) -> str: return hashlib.sha256(path.read_bytes()).hexdigest() @@ -106,8 +133,9 @@ def execute(args, items, settings) -> int: if args.out.exists(): rows = [json.loads(x) for x in args.out.read_text(encoding="utf-8").splitlines() if x.strip()] ids = {item["id"] for item in items} - done = {row["id"] for row in rows} - if len(done) != len(rows) or not done <= ids: + by_id = {row["id"]: row for row in rows} + done = {row["id"] for row in rows if complete_row(row)} + if len(by_id) != len(rows) or not set(by_id) <= ids: raise ValueError("Results have duplicate or unknown item IDs") hashes = { "source": hashlib.sha256((srcsimplex.SYSTEM_PROMPT + inspect.getsource(srcsimplex.passage_prompt)).encode()).hexdigest(), @@ -129,11 +157,24 @@ def execute(args, items, settings) -> int: elif rows: raise ValueError("Cannot resume results without their audit metadata") todo = [item for item in items if item["id"] not in done] + missing = sum(2 - int("role" in by_id.get(i["id"], {})) + - int("judge" in by_id.get(i["id"], {})) for i in todo) print(f"items={len(items)} done={len(done)} todo={len(todo)} model={settings.llm.model} " - f"nominal_calls={len(todo) * 2} request_attempts={meta['request_attempts']} cap={args.max_calls}") + f"missing_components={missing} request_attempts={meta['request_attempts']} cap={args.max_calls}") print("prompt_hashes:", json.dumps(hashes)) if args.dry_run: return 0 + if getattr(args, "audit_only", False): + meta["completed_items"] = len(done) + meta["processed_items"] = len(rows) + meta["status"] = ("provider_blocked" if any(provider_blocked(RuntimeError(message)) + for row in rows for message in row.get("errors", {}).values()) + else "detector_errors" if todo else "complete") + if args.out.exists(): + meta["results_sha256"] = digest(args.out) + atomic_json(meta_path, meta) + print(json.dumps(meta)) + return 0 if meta["status"] == "complete" else 2 if settings.llm.model != "qwen-max" or settings.llm.temperature != 0: raise ValueError("P0 is preregistered for qwen-max at temperature 0") client = AuditedClient.from_settings(settings.llm) @@ -142,6 +183,7 @@ def execute(args, items, settings) -> int: def checkpoint(): meta["usage"] = client.usage.as_dict() meta["completed_items"] = len(done) + meta["processed_items"] = len(by_id) atomic_json(meta_path, meta) def reserve(): @@ -155,19 +197,30 @@ def execute(args, items, settings) -> int: meta["max_calls"] = args.max_calls meta["status"] = "running" checkpoint() + def save_row(row): + by_id[row["id"]] = row + if complete_row(row): + done.add(row["id"]) + temporary = args.out.with_suffix(args.out.suffix + ".tmp") + with temporary.open("w", encoding="utf-8") as stream: + for item in items: + if item["id"] in by_id: + stream.write(json.dumps(by_id[item["id"]], ensure_ascii=False) + "\n") + stream.flush() + os.fsync(stream.fileno()) + os.replace(temporary, args.out) + checkpoint() + try: - with args.out.open("a", encoding="utf-8") as stream: - for item in todo: - row = run_item(client, item) - stream.write(json.dumps(row, ensure_ascii=False) + "\n") - stream.flush() - os.fsync(stream.fileno()) - done.add(item["id"]) - checkpoint() - print(f"completed={len(done)}/{len(items)} requests={meta['request_attempts']}", flush=True) - meta["status"] = "complete" - except CallBudgetExceeded as error: - meta["status"] = "budget_exhausted" + for item in todo: + row = run_item(client, item, by_id.get(item["id"])) + save_row(row) + print(f"completed={len(done)}/{len(items)} requests={meta['request_attempts']}", flush=True) + meta["status"] = "complete" if len(done) == len(items) else "detector_errors" + except (CallBudgetExceeded, ProviderBlocked) as error: + if getattr(error, "row", None) is not None: + save_row(error.row) + meta["status"] = "provider_blocked" if isinstance(error, ProviderBlocked) else "budget_exhausted" print(str(error), file=sys.stderr) except BaseException: meta["status"] = "interrupted" @@ -186,6 +239,7 @@ def main() -> int: ap.add_argument("--out", required=True, type=Path) ap.add_argument("--max-calls", type=int, default=400) ap.add_argument("--dry-run", action="store_true") + ap.add_argument("--audit-only", action="store_true", help="Reconcile saved state without making API calls") ap.add_argument("--labels", type=Path, help="Frozen labels; their hash is bound to the run") args = ap.parse_args() if not 1 <= args.max_calls <= 400: diff --git a/leanbench/schema.py b/leanbench/schema.py index b59f667..b81b5a7 100644 --- a/leanbench/schema.py +++ b/leanbench/schema.py @@ -1,4 +1,4 @@ -"""Roles and simplices: the parameters of a declaration as a small typed schema. +"""Semantic multi-role relation schemas, not geometric simplices. A Lean declaration is a bundle of roles: the objects it is about (``(G : Type*)``), the facts it assumes (``(h : a ∣ b)``), and the goal it asserts or the thing it @@ -8,8 +8,8 @@ be read off the prose of a book, so the two can be compared role by role. Design notes (from the archived ``schema-simplex`` prototype): * a role may be *constrained* to a closed set of allowed values (``choices``); -* a simplex is itself a role, so simplices nest (a lemma used by another is a role - of it), which is how a dependency structure appears; +* a simplex is itself a role, so explicitly supplied schemas can be composed; + nesting does not discover a proof dependency; * validation lives in ``__init__``. The prototype put it in a dataclass ``__post_init__`` next to a hand-written ``__init__``, where it never ran. """ @@ -41,7 +41,7 @@ class Role: choices: Sequence[Any] | None = None, attrs: dict[str, Any] | None = None, ) -> None: - if not name: + if not isinstance(name, str) or not name.strip(): raise ValueError("a role needs a name") if kind not in KINDS: raise ValueError(f"unknown role kind {kind!r}; expected one of {KINDS}") @@ -49,6 +49,8 @@ class Role: self.kind = kind self.type_text = type_text self.context = context + if isinstance(choices, (str, bytes)): + raise ValueError("choices must be a value sequence, not a string") self.choices: list[Any] | None = list(choices) if choices is not None else None self.attrs: dict[str, Any] = dict(attrs or {}) @@ -83,12 +85,21 @@ class Role: class Simplex(Role): """A reusable bundle of at least two roles, keyed by alias. Itself a role.""" - def __init__(self, name: str, roles: dict[str, Role], *, context: str = "") -> None: - super().__init__(name, KIND_SIMPLEX, context=context) + def __init__(self, name: str, roles: dict[str, Role], *, context: str = "", + attrs: dict[str, Any] | None = None) -> None: + super().__init__(name, KIND_SIMPLEX, context=context, attrs=attrs) if len(roles) < MIN_ROLES: raise ValueError( f"simplex {name!r} needs at least {MIN_ROLES} roles, got {len(roles)}" ) + if any(not isinstance(alias, str) or not alias or not isinstance(role, Role) + for alias, role in roles.items()): + raise ValueError("simplex slots need nonempty aliases and Role values") + for role in roles.values(): + references = role.attrs.get("references", []) + if (not isinstance(references, list) + or any(not isinstance(alias, str) or alias not in roles for alias in references)): + raise ValueError("role references must name slots in this simplex") self.roles = dict(roles) def by_kind(self, kind: str) -> list[Role]: @@ -105,16 +116,16 @@ class Simplex(Role): return out def as_dict(self) -> dict[str, Any]: - return { - "name": self.name, - "roles": {alias: role.as_dict() for alias, role in self.roles.items()}, - } + return {**super().as_dict(), + "roles": {alias: role.as_dict() for alias, role in self.roles.items()}} class State: """A role together with a value; unresolved until it has one.""" def __init__(self, role: Role, value: Any = None) -> None: + if value is not None: + role.check_value(value) self.role = role self.value = value @@ -133,3 +144,41 @@ class Fact(State): class Goal(State): """To be resolved.""" + + +def role_from_dict(data: dict[str, Any]) -> Role: + """Restore JSON role/schema data without executing code or loading pickle.""" + kind = data.get("kind", KIND_SIMPLEX if "roles" in data else KIND_OBJECT) + if kind == KIND_SIMPLEX: + return Simplex(data["name"], {alias: role_from_dict(role) + for alias, role in data["roles"].items()}, + context=data.get("context", ""), attrs=data.get("attrs")) + return Role(data["name"], kind, type_text=data.get("type", ""), + context=data.get("context", ""), choices=data.get("choices"), + attrs=data.get("attrs")) + + +class SimplexInstance: + """Values bind local slot aliases; a resolved goal is supplied, not proved here.""" + + def __init__(self, schema: Simplex, facts: dict[str, Any] | None = None, + goals: Sequence[str] | None = None) -> None: + self.schema = schema + facts = facts or {} + goal_aliases = list(goals) if goals is not None else [ + alias for alias, role in schema.roles.items() if role.kind in (KIND_GOAL, KIND_OWN)] + if (len(set(goal_aliases)) != len(goal_aliases) + or not (set(facts) | set(goal_aliases)) <= set(schema.roles) + or set(facts) & set(goal_aliases)): + raise ValueError("facts/goals need distinct, declared slot aliases") + self.facts = {alias: Fact(schema.roles[alias], value) for alias, value in facts.items()} + self.goals = {alias: Goal(schema.roles[alias]) for alias in goal_aliases} + + def resolve(self, alias: str, value: Any) -> None: + if alias not in self.goals or value is None: + raise ValueError("resolve needs a declared goal and a non-None value") + self.goals[alias].role.check_value(value) + self.goals[alias].value = value + + def is_completed(self) -> bool: + return bool(self.goals) and all(goal.is_resolved() for goal in self.goals.values()) diff --git a/leanbench/schema_registry.py b/leanbench/schema_registry.py new file mode 100644 index 0000000..77e173c --- /dev/null +++ b/leanbench/schema_registry.py @@ -0,0 +1,208 @@ +"""JSON/SQLite registry of semantic relation schemas and scoped slot occurrences. + +A role definition may be reused deliberately. Occurrences remain local to a +simplex: sharing a role definition never equates the objects bound to its aliases. +""" +from __future__ import annotations + +import fnmatch +import json +import sqlite3 +from collections.abc import Iterable, Mapping +from pathlib import Path +from urllib.parse import quote + +from .schema import KIND_GOAL, KIND_OWN, KIND_SIMPLEX, Role, Simplex, role_from_dict + + +def slot_key(parent: str, alias: str) -> str: + """An occurrence identity, distinct even when two slots reuse one definition.""" + return f"{parent}/slot/{quote(alias, safe='')}" + + +class SchemaRegistry: + """Immutable versioned records; reusing a key with changed content is rejected.""" + + def __init__(self, path: str | Path = ":memory:") -> None: + self.connection = sqlite3.connect(str(path)) + self.connection.execute("PRAGMA foreign_keys = ON") + self.connection.executescript(""" + CREATE TABLE IF NOT EXISTS schema_nodes ( + key TEXT PRIMARY KEY, + kind TEXT NOT NULL CHECK(kind IN ('role', 'simplex')), + payload TEXT NOT NULL + ); + CREATE TABLE IF NOT EXISTS schema_slots ( + parent TEXT NOT NULL REFERENCES schema_nodes(key) ON DELETE CASCADE, + alias TEXT NOT NULL, + child TEXT NOT NULL REFERENCES schema_nodes(key) ON DELETE RESTRICT, + position INTEGER NOT NULL, + PRIMARY KEY(parent, alias), + UNIQUE(parent, position) + ); + CREATE INDEX IF NOT EXISTS schema_slots_child ON schema_slots(child); + """) + + def __enter__(self): + return self + + def __exit__(self, *_): + self.close() + + def close(self) -> None: + self.connection.close() + + def _insert(self, key: str, kind: str, payload: dict) -> None: + if not isinstance(key, str) or not key: + raise ValueError("a registry key must be nonempty") + if (kind == "simplex") != (payload.get("kind") == KIND_SIMPLEX): + raise ValueError("nested simplex roles must use a Simplex object") + encoded = json.dumps(payload, sort_keys=True, ensure_ascii=False, allow_nan=False) + existing = self.connection.execute( + "SELECT kind, payload FROM schema_nodes WHERE key = ?", (key,)).fetchone() + if existing is not None and existing != (kind, encoded): + raise ValueError(f"key {key!r} already has different content; use a new version key") + self.connection.execute("INSERT OR IGNORE INTO schema_nodes VALUES (?, ?, ?)", + (key, kind, encoded)) + + def set_role(self, role: Role, key: str | None = None) -> str: + if isinstance(role, Simplex): + raise ValueError("use set_simplex for nested schemas") + key = key or f"role:{role.name}" + with self.connection: + self._insert(key, "role", role.as_dict()) + return key + + def set_simplex(self, simplex: Simplex, key: str | None = None, + role_keys: Mapping[str, str] | None = None) -> str: + """Default children are scoped. role_keys explicitly opts into definition reuse.""" + key = key or f"schema:{simplex.name}" + role_keys = dict(role_keys or {}) + if not set(role_keys) <= set(simplex.roles): + raise ValueError("reuse map has an unknown alias") + with self.connection: + self._put_simplex(simplex, key, role_keys, set()) + return key + + def _put_simplex(self, simplex: Simplex, key: str, reuse: dict[str, str], + active: set[int]) -> None: + if id(simplex) in active: + raise ValueError("cyclic simplex nesting") + active = active | {id(simplex)} + # Metadata only; children live in a relational slot table, not pickle blobs. + payload = Role.as_dict(simplex) + existing = self.connection.execute( + "SELECT key FROM schema_nodes WHERE key = ?", (key,)).fetchone() + if existing: + restored = self.get_simplex(key) + if restored is None or restored.as_dict() != simplex.as_dict(): + raise ValueError(f"key {key!r} already has different content; use a new version key") + expected = {alias: reuse.get(alias, slot_key(key, alias)) for alias in simplex.roles} + if self.slots(key) != expected: + raise ValueError("same schema key cannot change its role-definition references") + return + self._insert(key, "simplex", payload) + for position, (alias, child) in enumerate(simplex.roles.items()): + child_key = reuse.get(alias, slot_key(key, alias)) + if alias in reuse: + restored = self.get(child_key) + if restored is None or restored.as_dict() != child.as_dict(): + raise ValueError(f"reused role definition does not match slot {alias!r}") + elif isinstance(child, Simplex): + self._put_simplex(child, child_key, {}, active) + else: + self._insert(child_key, "role", child.as_dict()) + self.connection.execute("INSERT INTO schema_slots VALUES (?, ?, ?, ?)", + (key, alias, child_key, position)) + + def get(self, key: str) -> Role | None: + return self._get(key, set()) + + def _get(self, key: str, active: set[str]) -> Role | None: + if key in active: + raise ValueError("cyclic schema references in registry") + row = self.connection.execute( + "SELECT kind, payload FROM schema_nodes WHERE key = ?", (key,)).fetchone() + if row is None: + return None + kind, encoded = row + payload = json.loads(encoded) + if kind == "role": + return role_from_dict(payload) + slots = self.slots(key) + children = {alias: self._get(child, active | {key}) for alias, child in slots.items()} + return Simplex(payload["name"], children, context=payload.get("context", ""), + attrs=payload.get("attrs")) + + def get_role(self, key: str) -> Role | None: + value = self.get(key) + return value if not isinstance(value, Simplex) else None + + def get_simplex(self, key: str) -> Simplex | None: + value = self.get(key) + return value if isinstance(value, Simplex) else None + + def slots(self, key: str) -> dict[str, str]: + return dict(self.connection.execute( + "SELECT alias, child FROM schema_slots WHERE parent = ? ORDER BY position", (key,))) + + def keys(self, pattern: str = "*") -> list[str]: + return [key for (key,) in self.connection.execute("SELECT key FROM schema_nodes ORDER BY key") + if fnmatch.fnmatchcase(key, pattern)] + + def search_roles(self, query: str, limit: int = 10) -> list[dict]: + """Literal substring candidates; search does not authorize semantic reuse.""" + if not query.strip() or limit < 1: + return [] + found = [] + for key, payload in self.connection.execute( + "SELECT key, payload FROM schema_nodes WHERE kind = 'role' ORDER BY key"): + if query.casefold() in (key + payload).casefold(): + found.append({"key": key, "role": json.loads(payload)}) + if len(found) == limit: + break + return found + + def find_by_roles(self, role_keys: Iterable[str], match_all: bool = False) -> list[str]: + """Find schema keys containing definition keys, including nested descendants.""" + wanted = set(role_keys) + if not wanted: + return [] + found = [] + for key in self._simplex_keys(): + descendants = {row[0] for row in self.connection.execute(""" + WITH RECURSIVE descendants(child) AS ( + SELECT child FROM schema_slots WHERE parent = ? + UNION + SELECT slots.child FROM schema_slots slots JOIN descendants d ON slots.parent = d.child + ) SELECT child FROM descendants + """, (key,))} + matches = wanted <= descendants if match_all else bool(wanted & descendants) + if matches: + found.append(key) + return found + + def find_solvable(self, known_slots: Iterable[str]) -> list[dict]: + """Structural readiness by scoped occurrences, not proof or value unification.""" + known = set(known_slots) + candidates = [] + for key in self._simplex_keys(): + schema = self.get_simplex(key) + inputs, outputs = [], [] + for alias, role in schema.roles.items(): + target = outputs if role.kind in (KIND_GOAL, KIND_OWN) else inputs + target.append(slot_key(key, alias)) + missing_outputs = [output for output in outputs if output not in known] + if missing_outputs and set(inputs) <= known: + candidates.append({"schema_key": key, "input_slots": inputs, + "target_slots": missing_outputs, "structural_candidate_only": True}) + return candidates + + def _simplex_keys(self) -> list[str]: + return [row[0] for row in self.connection.execute( + "SELECT key FROM schema_nodes WHERE kind = 'simplex' ORDER BY key")] + + def info(self) -> dict[str, int]: + counts = dict(self.connection.execute("SELECT kind, count(*) FROM schema_nodes GROUP BY kind")) + return {"roles": counts.get("role", 0), "simplices": counts.get("simplex", 0), + "slots": self.connection.execute("SELECT count(*) FROM schema_slots").fetchone()[0]} diff --git a/tests/test_pilot_scripts.py b/tests/test_pilot_scripts.py index ee75b08..7cbcc17 100644 --- a/tests/test_pilot_scripts.py +++ b/tests/test_pilot_scripts.py @@ -141,3 +141,82 @@ def test_judge_rejects_string_boolean(): rp = load("run_pilot") with pytest.raises(ValueError, match="unusable judge"): rp.judge(ScriptedClient(['{"faithful": "false"}']), "passage", "code") + + +def test_partial_resume_keeps_successful_detector_output(): + rp = load("run_pilot") + row = rp.run_item(Stub(), ITEM) + expected_role = row["role"] + row.pop("judge") + row["errors"]["judge"] = "temporary failure" + + class JudgeOnly: + calls = 0 + + def complete_json(self, messages): + self.calls += 1 + assert "faithful" in messages[0]["content"] + return {"faithful": True} + + client = JudgeOnly() + resumed = rp.run_item(client, ITEM, row) + assert client.calls == 1 + assert resumed["role"] == expected_role + assert rp.complete_row(resumed) + assert row["errors"] == {"judge": "temporary failure"} + + +def test_billing_failure_stops_before_next_detector(): + import pytest + + from leanbench.llm import LLMError + + rp = load("run_pilot") + + class Blocked: + calls = 0 + + def complete_json(self, messages): + self.calls += 1 + raise LLMError("HTTP 400: Arrearage overdue-payment") + + client = Blocked() + with pytest.raises(rp.ProviderBlocked) as caught: + rp.run_item(client, ITEM) + assert client.calls == 1 + assert "role" in caught.value.row["errors"] + assert "judge" not in caught.value.row["errors"] + + +def test_blocked_run_preserves_and_replaces_partial_row(tmp_path, monkeypatch): + import argparse + import json + + from leanbench.config import Settings + + rp = load("run_pilot") + args = argparse.Namespace(items=tmp_path / "items.jsonl", out=tmp_path / "results.jsonl", + max_calls=400, dry_run=False) + args.items.write_text(json.dumps(ITEM) + "\n") + partial = {"id": "x1", "compiled": True, "role": {"flagged": False}, + "errors": {"judge": "Arrearage"}} + + def blocked(client, item, previous): + raise rp.ProviderBlocked(partial) + + monkeypatch.setattr(rp, "run_item", blocked) + assert rp.execute(args, [ITEM], Settings()) == 2 + meta = json.loads(args.out.with_suffix(".meta.json").read_text()) + assert meta["status"] == "provider_blocked" + assert meta["completed_items"] == 0 + + def recover(client, item, previous): + assert previous["role"] == partial["role"] + return {**previous, "judge": {"faithful": True}, "errors": {}} + + monkeypatch.setattr(rp, "run_item", recover) + assert rp.execute(args, [ITEM], Settings()) == 0 + rows = [json.loads(line) for line in args.out.read_text().splitlines()] + assert len(rows) == 1 and rp.complete_row(rows[0]) + meta = json.loads(args.out.with_suffix(".meta.json").read_text()) + assert meta["completed_items"] == 1 and meta["status"] == "complete" diff --git a/tests/test_schema_registry.py b/tests/test_schema_registry.py new file mode 100644 index 0000000..51d38ce --- /dev/null +++ b/tests/test_schema_registry.py @@ -0,0 +1,162 @@ +"""Semantic role definitions, scoped occurrences and structural candidate retrieval.""" +import json + +import pytest + +from leanbench.schema import ( + KIND_FACT, + KIND_GOAL, + Fact, + Role, + Simplex, + SimplexInstance, + role_from_dict, +) +from leanbench.schema_registry import SchemaRegistry, slot_key + + +def theorem(name="t"): + return Simplex(name, {"G": Role("group", context="A group carrier"), + "g": Role("element", type_text="G", attrs={"references": ["G"]}), + "finite": Role("finite", KIND_FACT, type_text="Finite G", + attrs={"references": ["G"]}), + "goal": Role("claim", KIND_GOAL, type_text="P G g", + attrs={"references": ["G", "g"]})}, + context="A multi-object claim", attrs={"provenance": "synthetic"}) + + +def test_json_roundtrip_keeps_metadata_and_nesting(): + outer = Simplex("outer", {"lemma": theorem(), "goal": Role("result", KIND_GOAL)}, + context="Composed relation", attrs={"version": 1}) + encoded = json.loads(json.dumps(outer.as_dict())) + restored = role_from_dict(encoded) + assert restored.as_dict() == outer.as_dict() + assert restored.roles["lemma"].roles["g"].attrs["references"] == ["G"] + + +def test_registry_persists_nested_schemas_in_one_transaction(tmp_path): + path = tmp_path / "registry.sqlite" + outer = Simplex("outer", {"lemma": theorem(), "goal": Role("result", KIND_GOAL)}) + with SchemaRegistry(path) as registry: + registry.set_simplex(outer) + registry.set_simplex(outer) + assert registry.info() == {"roles": 5, "simplices": 2, "slots": 6} + with SchemaRegistry(path) as registry: + assert registry.get_simplex("schema:outer").as_dict() == outer.as_dict() + leaf = slot_key(slot_key("schema:outer", "lemma"), "g") + assert registry.find_by_roles([leaf], match_all=True) == [ + "schema:outer", slot_key("schema:outer", "lemma")] + + +def test_same_names_in_different_theorems_are_scoped(): + with SchemaRegistry() as registry: + registry.set_simplex(theorem("first")) + registry.set_simplex(theorem("second")) + first_group = slot_key("schema:first", "G") + assert registry.find_by_roles([first_group]) == ["schema:first"] + assert registry.get_role(first_group).name == "group" + assert registry.slots("schema:first")["G"] != registry.slots("schema:second")["G"] + + +def test_explicit_reuse_does_not_equate_local_bindings_or_multiplicity(): + group = Role("group") + schema = Simplex("isomorphism", {"left": group, "right": group, + "goal": Role("equivalence", KIND_GOAL)}) + with SchemaRegistry() as registry: + registry.set_role(group, "role:group") + registry.set_simplex(schema, role_keys={"left": "role:group", "right": "role:group"}) + assert registry.slots("schema:isomorphism")["left"] == "role:group" + assert registry.find_solvable(["role:group"]) == [] + assert registry.find_solvable([slot_key("schema:isomorphism", "left")]) == [] + candidate = registry.find_solvable([slot_key("schema:isomorphism", x) for x in ["left", "right"]]) + assert candidate[0]["target_slots"] == [slot_key("schema:isomorphism", "goal")] + instance = SimplexInstance(schema, {"left": "C2", "right": "C3"}) + assert instance.facts["left"].value != instance.facts["right"].value + assert not instance.is_completed() + instance.resolve("goal", "a supplied result, not checked by the registry") + assert instance.is_completed() + + +def test_premise_is_required_and_known_goal_is_not_a_missing_target(): + with SchemaRegistry() as registry: + registry.set_simplex(theorem()) + inputs = [slot_key("schema:t", alias) for alias in ["G", "g", "finite"]] + assert registry.find_solvable(inputs[:-1]) == [] + assert registry.find_solvable(inputs)[0]["structural_candidate_only"] + assert registry.find_solvable(inputs + [slot_key("schema:t", "goal")]) == [] + + +def test_failed_write_rolls_back_every_child(): + with SchemaRegistry() as registry: + registry.set_role(Role("incompatible"), "role:shared") + before = registry.info() + with pytest.raises(ValueError, match="does not match"): + registry.set_simplex(theorem(), role_keys={"goal": "role:shared"}) + assert registry.info() == before + assert registry.get_simplex("schema:t") is None + + +def test_cyclic_nesting_is_rejected_without_partial_write(): + schema = Simplex("cycle", {"a": Role("a"), "b": Role("b")}) + schema.roles["b"] = schema + with SchemaRegistry() as registry: + with pytest.raises(ValueError, match="cyclic"): + registry.set_simplex(schema) + assert registry.info() == {"roles": 0, "simplices": 0, "slots": 0} + + +def test_keys_are_immutable_and_reuse_map_cannot_silently_change(): + with SchemaRegistry() as registry: + registry.set_role(Role("G"), "role:G") + with pytest.raises(ValueError, match="different content"): + registry.set_role(Role("H"), "role:G") + schema = theorem() + registry.set_simplex(schema) + registry.set_role(schema.roles["G"], "role:shared") + with pytest.raises(ValueError, match="cannot change"): + registry.set_simplex(schema, role_keys={"G": "role:shared"}) + assert registry.search_roles("%") == [] + assert registry.search_roles("group", limit=1)[0]["role"]["name"] == "group" + + +def test_instance_constraints_unknown_slots_and_invalid_references(): + role = Role("parity", choices=["even", "odd"]) + with pytest.raises(ValueError, match="not allowed"): + Fact(role, "prime") + schema = Simplex("pair", {"input": role, "goal": Role("result", KIND_GOAL, choices=[True])}) + instance = SimplexInstance(schema, {"input": "even"}) + with pytest.raises(ValueError, match="not allowed"): + instance.resolve("goal", False) + with pytest.raises(ValueError, match="declared"): + SimplexInstance(schema, {"unknown": "value"}) + with pytest.raises(ValueError, match="references"): + Simplex("invalid", {"x": Role("x", attrs={"references": ["missing"]}), "y": Role("y")}) + with pytest.raises(ValueError, match="name"): + Role(" ") + with pytest.raises(ValueError, match="sequence"): + Role("choice", choices="even") + with SchemaRegistry() as registry, pytest.raises(ValueError, match="Simplex object"): + registry.set_role(Role("fake", "simplex")) + + +def test_pilot_materialization_keeps_partial_lean_projection_explicit(): + import importlib.util + from pathlib import Path + + path = Path(__file__).resolve().parents[1] / "experiments/P0-pilot/build_schemas.py" + spec = importlib.util.spec_from_file_location("build_schemas", path) + builder = importlib.util.module_from_spec(spec) + spec.loader.exec_module(builder) + items = [{"id": "closed", "lean_code": "theorem t : True := trivial"}] + assessment = {"records": [{"id": "closed", "blind_id": "P01", "source": { + "roles": [{"kind": "object", "symbols": ["G"], "description": "group"}, + {"kind": "goal", "description": "A synthetic claim"}]}}]} + with SchemaRegistry() as registry: + index, snapshots = builder.build(items, assessment, {"P01": "closed"}, registry) + assert registry.info()["simplices"] == 1 + assert index[0]["source_status"] == "unreviewed_annotation_seed" + assert index[0]["lean_schema"] is None + assert index[0]["lean_status"] == "insufficient_projected_roles" + assert snapshots[0]["lean_projection"]["roles"][0]["kind"] == "goal" + with pytest.raises(ValueError, match="exactly once"): + builder.build(items, {"records": []}, {"P01": "closed"}, registry)