[wip] Mathlib integration

packages/core/src/Bundle.ts

@@ -17,6 +17,9 @@ export type Bundle = {
   spaces: Map<Id, Space>
   traits: Map<Id, Trait<Id>>
   theorems: Map<Id, Theorem>
+  lean?: {
+    properties: { id: string; module: string }[]
+  }
   version: Version
 }
 
@@ -26,6 +29,16 @@ export const serializedSchema = z.object({
   theorems: z.array(theoremSchema),
   traits: z.array(traitSchema(z.string())),
   version: z.object({ ref: z.string(), sha: z.string() }),
+  lean: z
+    .object({
+      properties: z.array(
+        z.object({
+          id: z.string(),
+          module: z.string(),
+        }),
+      ),
+    })
+    .optional(),
 })
 
 export type Serialized = z.infer<typeof serializedSchema>
@@ -41,14 +54,16 @@ export function serialize(bundle: Bundle): Serialized {
 }
 
 export function deserialize(data: unknown): Bundle {
-  const serialized = serializedSchema.parse(data)
+  const { properties, spaces, theorems, traits, version, lean } =
+    serializedSchema.parse(data)
 
   return {
-    properties: indexBy(serialized.properties, p => p.uid),
-    spaces: indexBy(serialized.spaces, s => s.uid),
-    theorems: indexBy(serialized.theorems, t => t.uid),
-    traits: indexBy(serialized.traits, traitId),
-    version: serialized.version,
+    properties: indexBy(properties, p => p.uid),
+    spaces: indexBy(spaces, s => s.uid),
+    theorems: indexBy(theorems, t => t.uid),
+    traits: indexBy(traits, traitId),
+    lean,
+    version,
   }
 }
 

packages/core/src/Property.ts

@@ -5,6 +5,7 @@ export const propertySchema = z.intersection(
   z.object({
     name: z.string(),
     aliases: z.array(z.string()),
+    mathlib: z.string().optional(),
   }),
   recordSchema,
 )

packages/viewer/src/components/Properties/Show.svelte

@@ -9,6 +9,11 @@
   export let rel: string | undefined = undefined
 
   const tabs = ['spaces', 'theorems', 'references'] as const
+
+  function leanUrl({ id, module }: { id: string; module: string }) {
+    const path = module.replaceAll('.', '/')
+    return `https://leanprover-community.github.io/mathlib4_docs/${path}.html#${id}`
+  }
 </script>
 
 <Title title={property.name} />
@@ -24,6 +29,16 @@
   <Typeset body={property.description} />
 </section>
 
+{#if property?.lean}
+  <section>
+    <a href={leanUrl(property.lean)} target="_blank">
+      Formalized in Lean as <code>{property.lean.id}</code>
+      in
+      <code>{property.lean.module}</code>
+    </a>
+  </section>
+{/if}
+
 <Tabs {tabs} {tab} {rel} />
 
 {#if tab === 'spaces'}

packages/viewer/src/gateway.ts

@@ -31,11 +31,18 @@ export function sync(
     trace({ event: 'remote_fetch_started', host, branch })
     const result = await pb.bundle.fetch({ host, branch, etag, fetch })
 
+    const propIdx: Record<string, string> = {}
+    if (result?.bundle.lean?.properties) {
+      for (const { id, module } of result.bundle.lean.properties) {
+        propIdx[id] = module
+      }
+    }
+
     if (result) {
       trace({ event: 'remote_fetch_complete', result })
       return {
         spaces: transform(space, result.bundle.spaces),
-        properties: transform(property, result.bundle.properties),
+        properties: transform(property(propIdx), result.bundle.properties),
         traits: transform(trait, result.bundle.traits),
         theorems: transform(theorem, result.bundle.theorems),
         etag: result.etag,
@@ -47,19 +54,28 @@ export function sync(
   }
 }
 
-function property({
-  uid,
-  name,
-  aliases,
-  description,
-  refs,
-}: pb.Property): Property {
-  return {
-    id: Id.toInt(uid),
+function property(propertyIdx: Record<string, string>) {
+  return function ({
+    uid,
     name,
     aliases,
     description,
     refs,
+    mathlib,
+  }: pb.Property): Property {
+    return {
+      id: Id.toInt(uid),
+      name,
+      aliases,
+      description,
+      refs,
+      lean: mathlib
+        ? {
+            id: mathlib,
+            module: propertyIdx[mathlib],
+          }
+        : undefined,
+    }
   }
 }
 

packages/viewer/src/types/index.ts

@@ -9,6 +9,10 @@ export type Property = {
   aliases: string[]
   description: string
   refs: Ref[]
+  lean?: {
+    id: string
+    module: string
+  }
 }
 
 export type Space = {