addedOutput schema / $defs / LeanStatement
Added value: +{
+ "properties": {
+ "anchor_verdict": {
+ "title": "Anchor Verdict",
+ "type": "string"
+ },
+ "decl": {
+ "title": "Decl",
+ "type": "string"
+ },
+ "label": {
+ "title": "Label",
+ "type": "string"
+ },
+ "lean_statement": {
+ "title": "Lean Statement",
+ "type": "string"
+ },
+ "paper_claim_key": {
+ "anyOf": [
+ {
+ "type": "string"
+ },
+ {
+ "type": "null"
+ }
+ ],
+ "title": "Paper Claim Key"
+ },
+ "referee_judgments": {
+ "items": {
+ "additionalProperties": true,
+ "type": "object"
+ },
+ "title": "Referee Judgments",
+ "type": "array"
+ }
+ },
+ "required": [
+ "decl",
+ "label",
+ "lean_statement",
+ "paper_claim_key",
+ "anchor_verdict",
+ "referee_judgments"
+ ],
+ "title": "LeanStatement",
+ "type": "object"
+}
addedOutput schema / $defs / LeanSummary
Added value: +{
+ "description": "The paper's latest Lean build on Pith and published referees' sign-offs on it.",
+ "properties": {
+ "mathlib": {
+ "anyOf": [
+ {
+ "type": "string"
+ },
+ {
+ "type": "null"
+ }
+ ],
+ "title": "Mathlib"
+ },
+ "note": {
+ "title": "Note",
+ "type": "string"
+ },
+ "statements": {
+ "items": {
+ "$ref": "#/$defs/LeanStatement"
+ },
+ "title": "Statements",
+ "type": "array"
+ },
+ "status": {
+ "title": "Status",
+ "type": "string"
+ },
+ "toolchain": {
+ "anyOf": [
+ {
+ "type": "string"
+ },
+ {
+ "type": "null"
+ }
+ ],
+ "title": "Toolchain"
+ }
+ },
+ "required": [
+ "status",
+ "toolchain",
+ "mathlib",
+ "statements",
+ "note"
+ ],
+ "title": "LeanSummary",
+ "type": "object"
+}
addedOutput schema / properties / lean
Added value: +{
+ "anyOf": [
+ {
+ "$ref": "#/$defs/LeanSummary"
+ },
+ {
+ "type": "null"
+ }
+ ]
+}