diff --git a/examples/website/DemoSiteMain.lean b/examples/website/DemoSiteMain.lean
index fa6416edc..897250fcb 100644
--- a/examples/website/DemoSiteMain.lean
+++ b/examples/website/DemoSiteMain.lean
@@ -9,6 +9,8 @@ import DemoSite
 
 open Verso Genre Blog Site Syntax
 
+set_option verso.literateMarkdown.convertDoccomments true 
+
 open Output Html Template Theme in
 def theme : Theme := { Theme.default with
   primaryTemplate := do
diff --git a/src/verso-blog/VersoBlog/LiterateLeanPage.lean b/src/verso-blog/VersoBlog/LiterateLeanPage.lean
index 9fae21a30..80fb2873d 100644
--- a/src/verso-blog/VersoBlog/LiterateLeanPage.lean
+++ b/src/verso-blog/VersoBlog/LiterateLeanPage.lean
@@ -312,19 +312,24 @@ section
 variable [Monad m] [MonadError m] [MonadQuotation m]
 
 
-partial def getModuleDocString (hl : Highlighted) : m String := do
+
+partial def getCommentString (pref : String) (hl : Highlighted) : m String := do
   let str := (← getString hl).trim
-  let str := str.stripPrefix "/-!" |>.stripSuffix "-/" |>.trim
+  let str := str.stripPrefix pref |>.stripSuffix "-/" |>.trim
   pure str
 where getString : Highlighted → m String
   | .text txt => pure txt
   | .tactics .. => throwError "Tactics found in module docstring!"
   | .point .. => pure ""
-  | .span _ hl => getModuleDocString hl
+  | .span _ hl => getCommentString pref hl
   | .seq hls => do return (← hls.mapM getString).foldl (init := "") (· ++ ·)
   | .token ⟨_, txt⟩ => pure txt
+
+partial def getModuleDocString : Highlighted -> m String := getCommentString "/-!"
+partial def getDocCommentString : Highlighted -> m String := getCommentString "/--"
 end
 
+
 def getFirstMessage : Highlighted → Option (Highlighted.Span.Kind × String)
   | .span msgs x =>
     msgs[0]? <|> getFirstMessage x
@@ -394,6 +399,30 @@ partial def docFromMod (project : System.FilePath) (mod : String)
           }
         | other =>
           addBlock (← ofBlock helper other)
+    -- Lemma is purposefully unchecked, such that it can be matched on when a project
+    -- is dependent on mathlib
+    | ``declaration | `lemma =>
+      -- Only convert doccomments if the option is turned on
+      match (← getConvertDoccomments), code with
+      | true, .seq s =>
+        -- Find the index corresponding to the docComment
+        let docCommentIdx := s.findIdx? (fun
+          | (.token ⟨.docComment, _⟩) => true
+          | _ => false)
+        match docCommentIdx with
+        | some i =>
+          let codeBefore ← ``(Block.other
+            (BlockExt.highlightedCode `name $(quote (Highlighted.seq s[:i]))) Array.mkArray0)
+          let some ⟨mdBlocks⟩ := MD4Lean.parse (← getDocCommentString s[i]!)
+            | throwError m!"Failed to parse Markdown: {← getDocCommentString s[i]!}"
+          let docCommentBlocks ← mdBlocks.mapM (fun b => ofBlock helper b)
+          let codeAfter ←``(Block.other (BlockExt.highlightedCode `name $(quote (Highlighted.seq s[i+1:]))) Array.mkArray0)
+          let blocks := #[codeBefore] ++ docCommentBlocks ++ #[codeAfter]
+          addBlock (← ``(Block.other (BlockExt.htmlDiv "declaration") #[$blocks,*]))
+        | none =>
+          -- No docComment attached to declaration, render definition as usual
+          addBlock (← ``(Block.other (BlockExt.highlightedCode `name $(quote code)) Array.mkArray0))
+      | _, _ => addBlock (← ``(Block.other (BlockExt.highlightedCode `name $(quote code)) Array.mkArray0))
     | ``eval | ``evalBang | ``reduceCmd | ``print | ``printAxioms | ``printEqns | ``«where» | ``version | ``synth | ``check =>
       addBlock (← ``(Block.other (BlockExt.highlightedCode `name $(quote code)) Array.mkArray0))
       if let some (k, msg) := getFirstMessage code then
@@ -585,6 +614,8 @@ directory that contains a toolchain file and a Lake configuration (`lakefile.tom
 
 Set the option `verso.literateMarkdown.logInlines` to `true` to see the error messages that
 prevented elaboration of inline elements.
+Set the option `verso.literateMarkdown.convertDoccomments` to `true` to convert doccomments in
+a similar way as the module docstrings, except without allowing headers.
 -/
 syntax "def_literate_post " ident optConfig " from " ident " in " str " as " str (" with " term)? (rewrites)? : command
 
diff --git a/src/verso-blog/VersoBlog/LiterateLeanPage/Options.lean b/src/verso-blog/VersoBlog/LiterateLeanPage/Options.lean
index 0ad40f33e..4b78c524e 100644
--- a/src/verso-blog/VersoBlog/LiterateLeanPage/Options.lean
+++ b/src/verso-blog/VersoBlog/LiterateLeanPage/Options.lean
@@ -13,7 +13,17 @@ register_option verso.literateMarkdown.logInlines : Bool := {
   descr := "Whether to log failures to elaborate inline code items in Markdown comments."
 }
 
+register_option verso.literateMarkdown.convertDoccomments : Bool := {
+  defValue := false
+  group := "doc"
+  descr := "Whether to convert doccomments on definitions to text ."
+}
+
+
 namespace Verso.Genre.Blog.Literate
 
 def getLogInlines [Monad m] [MonadOptions m] : m Bool := do
   return (← getOptions).get verso.literateMarkdown.logInlines.name verso.literateMarkdown.logInlines.defValue
+
+def getConvertDoccomments [Monad m] [MonadOptions m] : m Bool := do
+  return (← getOptions).get verso.literateMarkdown.convertDoccomments.name verso.literateMarkdown.convertDoccomments.defValue