diff --git a/src/emacs/lean-mmm-lua.el b/src/emacs/lean-mmm-lua.el
new file mode 100644
index 000000000..73970363d
--- /dev/null
+++ b/src/emacs/lean-mmm-lua.el
@@ -0,0 +1,25 @@
+;; Copyright (c) 2013, 2014 Microsoft Corporation. All rights reserved.
+;; Released under Apache 2.0 license as described in the file LICENSE.
+;;
+;; Author: Soonho Kong
+;;
+
+(when (and (package-installed-p 'mmm-mode)
+           (package-installed-p 'lua-mode))
+  (require 'mmm-mode)
+  (require 'mmm-auto)
+  (require 'lua-mode)
+  (setq mmm-global-mode 'buffers-with-submode-classes)
+  (setq mmm-submode-decoration-level 0)
+  (eval-after-load 'mmm-vars
+    '(progn
+       (mmm-add-group
+        'lean-lua
+        '((lua-inline
+           :submode lua-mode
+           :face mmm-code-submode-face
+           :front "[(][*]"
+           :back "[*][)]")))
+       (mmm-add-mode-ext-class 'lean-mode "\\.lean" 'lean-lua))))
+
+(provide 'lean-mmm-lua)
diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index 8b1cc166a..56d50bf14 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -25,6 +25,7 @@
 (require 'lean-tags)
 (require 'lean-option)
 (require 'lean-syntax)
+(require 'lean-mmm-lua)
 
 (defun lean-compile-string (exe-name args file-name)
   "Concatenate exe-name, args, and file-name"