diff --git a/HepLean/Meta/Informal.lean b/HepLean/Meta/Informal.lean
index 86b5046..b75bde8 100644
--- a/HepLean/Meta/Informal.lean
+++ b/HepLean/Meta/Informal.lean
@@ -13,6 +13,8 @@ open Lean Elab System
 
 /-! TODO: Derive a means to extract informal definitions and informal lemmas. -/
 
+/-! TODO: Can likely make this a bona-fide command. -/
+
 /-- The structure representating an informal definition. -/
 structure InformalDefinition where
   /-- The name of the informal definition. This is autogenerated. -/
@@ -21,6 +23,8 @@ structure InformalDefinition where
   math : String
   /-- The physics description of the definition. -/
   physics : String
+  /-- References. -/
+  ref : String
 
 /-- The structure representating an informal proof. -/
 structure InformalLemma where
@@ -32,6 +36,8 @@ structure InformalLemma where
   physics : String
   /-- A description of the proof. -/
   proof : String
+  /-- References. -/
+  ref : String
 
 namespace Informal
 
@@ -49,6 +55,7 @@ syntax (name := informal_definition) "informal_definition " ident
 macro "informal_definition " name:ident " where " assignments:informalAssignment* : command => do
   let mut math_def? : Option (TSyntax `term) := none
   let mut physics_def? : Option (TSyntax `term) := none
+  let mut ref_def? : Option (TSyntax `term) := none
   for assignment in assignments do
     match assignment with
     | `(informalAssignment| physics :≈ $val:str) =>
@@ -57,15 +64,19 @@ macro "informal_definition " name:ident " where " assignments:informalAssignment
     | `(informalAssignment| math :≈ $val:str) =>
       let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for math"
       math_def? := some (← `($(Lean.quote strVal)))
+    | `(informalAssignment| ref :≈ $val:str) =>
+      let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for ref"
+      ref_def? := some (← `($(Lean.quote strVal)))
     | _ => Macro.throwError "invalid assignment syntax"
-  unless physics_def?.isSome && math_def?.isSome do
-    Macro.throwError "Both 'physics' and 'math' assignments are required"
+  unless math_def?.isSome do
+    Macro.throwError "A 'math' assignments is required"
   `(
 /-- An informal definition. -/
 def $name : InformalDefinition := {
   name := $(Lean.quote name.getId),
   physics := $(physics_def?.getD (← `("No physics description provided"))),
-  math := $(math_def?.getD (panic! "math not assigned"))
+  math := $(math_def?.getD (panic! "math not assigned")),
+  ref := $(ref_def?.getD (← `("No references provided")))
     })
 
 /-- The syntax for the command `informal_lemma`. -/
@@ -77,6 +88,7 @@ macro "informal_lemma " name:ident " where " assignments:informalAssignment* : c
   let mut math_def? : Option (TSyntax `term) := none
   let mut physics_def? : Option (TSyntax `term) := none
   let mut proof_def? : Option (TSyntax `term) := none
+  let mut ref_def? : Option (TSyntax `term) := none
   for assignment in assignments do
     match assignment with
     | `(informalAssignment| physics :≈ $val:str) =>
@@ -88,9 +100,12 @@ macro "informal_lemma " name:ident " where " assignments:informalAssignment* : c
     | `(informalAssignment| proof :≈ $val:str) =>
       let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for proof"
       proof_def? := some (← `($(Lean.quote strVal)))
+    | `(informalAssignment| ref :≈ $val:str) =>
+      let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for ref"
+      ref_def? := some (← `($(Lean.quote strVal)))
     | _ => Macro.throwError "invalid assignment syntax"
   unless math_def?.isSome do
-    Macro.throwError "Both 'physics' and 'math' assignments are required"
+    Macro.throwError "A 'math' assignments is required"
   `(
 /-- An informal lemma. -/
 def $name : InformalLemma := {
@@ -98,6 +113,7 @@ def $name : InformalLemma := {
   physics := $(physics_def?.getD (← `("No physics description provided"))),
   math := $(math_def?.getD (panic! "math not assigned")),
   proof := $(proof_def?.getD (← `("No proof description provided"))),
+  ref := $(ref_def?.getD (← `("No references provided")))
     })
 
 end Informal