diff --git a/Auto/EvaluateAuto/TestAuto.lean b/Auto/EvaluateAuto/TestAuto.lean
index 426f058..4c16414 100644
--- a/Auto/EvaluateAuto/TestAuto.lean
+++ b/Auto/EvaluateAuto/TestAuto.lean
@@ -279,4 +279,34 @@ where
       ]
     String.intercalate "\n" lines
 
+/--
+  Read results generated by `evalAutoAtMathlibHumanTheorems`
+-/
+def readAutoEvalResult (config : EvalAutoOnMathlibConfig) :
+  CoreM (Array (Name × Result)) := do
+  let resultFolder := config.resultFolder
+  if !(← System.FilePath.isDir resultFolder) then
+    throwError "{decl_name%} :: {config.resultFolder} is not a directory"
+  let allFiles := (← System.FilePath.readDir resultFolder).map IO.FS.DirEntry.path
+  let mut ret := #[]
+  for file in allFiles do
+    if !(← System.FilePath.isDir file) && file.toString.takeRight 7 == ".result" then
+      let content ← IO.FS.readFile file
+      let lines := content.splitOn "\n"
+      if lines[2]? != .some "Summary:" || lines[3]? != .some "" then
+        throwError "{decl_name%} :: Format of result file changed, please change analysis code. Result file : {file}"
+      let lines := (lines.drop 4).filter (fun s => s != "")
+      let lineAnalysis ← (Array.mk lines).mapM analyzeLine
+      ret := ret.append lineAnalysis
+  return ret
+where
+  analyzeLine (line : String) : CoreM (Name × Result) := do
+    let line := (line.dropWhile (fun c => c != ' ')).drop 1
+    let s := line.takeWhile (fun c => c != ' ')
+    let .some tr := Result.ofConcise? s
+      | throwError s!"{decl_name%} :: {s} is not a concise representation of a `Result`"
+    let line := (line.dropWhile (fun c => c != ' ')).drop 2
+    let name := Name.parseUniqRepr line
+    return (name, tr)
+
 end EvalAuto