diff --git a/src/statement.rs b/src/statement.rs
index f2aa29e..e4a6d15 100644
--- a/src/statement.rs
+++ b/src/statement.rs
@@ -5,6 +5,7 @@ use crate::uni::UnicodeRenderer;
 use handlebars::Handlebars;
 use metamath_knife::comment_parser::CommentItem;
 use metamath_knife::comment_parser::CommentParser;
+use metamath_knife::grammar::FormulaToken;
 use metamath_knife::proof::ProofTreeArray;
 use metamath_knife::statement::as_str;
 use metamath_knife::statement::StatementRef;
@@ -87,16 +88,50 @@ impl ExpressionRenderer {
     ) -> Result<String, String> {
         match self {
             ExpressionRenderer::Ascii => self.render_formula(
-                database
-                    .stmt_parse_result()
-                    .get_formula(sref)
-                    .ok_or("Formula not found")?,
+                &self.get_formula(sref, database, use_provables)?,
                 database,
                 use_provables,
             ),
             ExpressionRenderer::Unicode(uni) => uni.render_statement(sref),
             #[cfg(feature = "sts")]
-            ExpressionRenderer::Sts(sts) => sts.render_statement(sref, use_provables),
+            ExpressionRenderer::Sts(sts) => sts.render_formula(
+                &self.get_formula(sref, database, use_provables)?,
+                use_provables,
+            ),
+        }
+    }
+
+    #[inline]
+    fn get_formula(
+        &self,
+        sref: &StatementRef,
+        database: &Database,
+        use_provables: bool,
+    ) -> Result<Formula, String> {
+        if use_provables {
+            database
+                .stmt_parse_result()
+                .get_formula(sref)
+                .ok_or("Unknown statement".into())
+                .cloned()
+        } else {
+            let nset = database.name_result();
+            let grammar = database.grammar_result();
+            let mut tokens = sref.math_iter();
+            let _typecode = nset.get_atom(&tokens.next().unwrap());
+            grammar
+                .parse_formula(
+                    &mut tokens.map(|t| {
+                        Ok(FormulaToken {
+                            symbol: nset.get_atom(&t),
+                            span: metamath_knife::Span::NULL,
+                        })
+                    }),
+                    &grammar.typecodes(),
+                    true,
+                    nset,
+                )
+                .map_err(|e| format!("Could not parse formula (GF): {}", e))
         }
     }
 
@@ -104,11 +139,16 @@ impl ExpressionRenderer {
         &self,
         formula: &Formula,
         database: &Database,
-        #[allow(unused_variables)] use_provables: bool,
+        use_provables: bool,
     ) -> Result<String, String> {
         match self {
             ExpressionRenderer::Ascii => {
-                Ok(format!("<pre>{}</pre>", formula.as_ref(database)).replace("wff ", " |- "))
+                let s = format!("<pre>{}</pre>", formula.as_ref(database));
+                Ok(if use_provables {
+                    s.replace("wff ", " |- ")
+                } else {
+                    s
+                })
             }
             ExpressionRenderer::Unicode(uni) => uni.render_formula(formula),
             #[cfg(feature = "sts")]
diff --git a/src/sts.rs b/src/sts.rs
index 869740c..f68da9e 100644
--- a/src/sts.rs
+++ b/src/sts.rs
@@ -3,7 +3,6 @@ use metamath_knife::formula::Substitutions;
 use metamath_knife::formula::TypeCode;
 use metamath_knife::grammar::FormulaToken;
 use metamath_knife::statement::as_str;
-use metamath_knife::statement::StatementRef;
 use metamath_knife::Database;
 use metamath_knife::Formula;
 use metamath_knife::StatementType;
@@ -131,21 +130,16 @@ impl StsDefinition {
         } else {
             formula.get_typecode()
         };
+        let mut mathml = self.format(typecode, formula)?;
+        if !use_provables && typecode != grammar.provable_typecode() {
+            mathml = format!(
+                "<mrow><mo mathcolor=#CCC>{}</mo> {}</mrow>",
+                as_str(self.database.name_result().atom_name(typecode)),
+                self.format(formula.get_typecode(), formula)?
+            );
+        }
         let display = self.display.clone();
-        Ok(display.replace("###", &self.format(typecode, formula)?))
-    }
-
-    pub fn render_statement(
-        &self,
-        sref: &StatementRef,
-        use_provables: bool,
-    ) -> Result<String, String> {
-        let formula = self
-            .database
-            .stmt_parse_result()
-            .get_formula(sref)
-            .ok_or("Unknown statement")?;
-        self.render_formula(formula, use_provables)
+        Ok(display.replace("###", &mathml))
     }
 
     pub fn check(&self) {