diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean
index 4db1c6a691..a39bd19c4e 100644
--- a/src/Init/Data/Float.lean
+++ b/src/Init/Data/Float.lean
@@ -98,4 +98,4 @@ abbrev Nat.toFloat (n : Nat) : Float :=
 
 instance : Pow Float := ⟨Float.pow⟩
 
-@[extern "lean_float_of_decimal"] constant Float.ofDecimal (m : Nat) (e : Nat) : Float
+@[extern "lean_float_of_decimal"] constant Float.ofDecimal (m : Nat) (s : Bool) (e : Nat) : Float
diff --git a/src/Init/Data/OfDecimal.lean b/src/Init/Data/OfDecimal.lean
index 0498e55a00..a4d097a140 100644
--- a/src/Init/Data/OfDecimal.lean
+++ b/src/Init/Data/OfDecimal.lean
@@ -8,10 +8,13 @@ import Init.Data.Float
 import Init.Data.Nat
 
 /- For decimal numbers (e.g., `1.23`).
-   The Lean frontend uses `OfDecimal.ofDecimal 123 2` to represent `1.23` -/
+   Examples:
+   - `OfDecimal.ofDecimal 123 true 2`    represents `1.23`
+   - `Ofdecimal.ofdecimal 121 false 100` represents `121e100`
+-/
 class OfDecimal (α : Type u) where
-  ofDecimal : Nat → Nat → α
+  ofDecimal : Nat → Bool → Nat → α
 
 @[defaultInstance]
 instance : OfDecimal Float where
-  ofDecimal m e := Float.ofDecimal m e
+  ofDecimal m s e := Float.ofDecimal m s e
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 5dd4abe46a..93f52815bb 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -288,9 +288,6 @@ def mkNumLit (val : String) (info : SourceInfo := {}) : Syntax :=
 def mkDecimalLit (val : String) (info : SourceInfo := {}) : Syntax :=
   mkLit decimalLitKind val info
 
-def mkScientificLit (val : String) (info : SourceInfo := {}) : Syntax :=
-  mkLit scientificLitKind val info
-
 /- Recall that we don't have special Syntax constructors for storing numeric and string atoms.
    The idea is to have an extensible approach where embedded DSLs may have new kind of atoms and/or
    different ways of representing them. So, our atoms contain just the parsed string.
@@ -373,28 +370,64 @@ def isNatLit? (s : Syntax) : Option Nat :=
 def isFieldIdx? (s : Syntax) : Option Nat :=
   isNatLitAux fieldIdxKind s
 
-partial def decodeDecimalLitVal? (s : String) : Option (Nat × Nat) :=
+partial def decodeDecimalLitVal? (s : String) : Option (Nat × Bool × Nat) :=
   let len := s.length
   if len == 0 then none
   else
     let c := s.get 0
     if c.isDigit then
-      decode 0 0 0 false
+      decode 0 0
     else none
 where
-  decode (i : String.Pos) (val : Nat) (e : Nat) (foundDot : Bool) : Option (Nat × Nat) :=
+  decodeAfterExp (i : String.Pos) (val : Nat) (e : Nat) (sign : Bool) (exp : Nat) : Option (Nat × Bool × Nat) :=
     if s.atEnd i then
-      if foundDot then some (val, e) else none
+      if sign then
+        some (val, sign, exp + e)
+      else if exp >= e then
+        some (val, sign, exp - e)
+      else
+        some (val, true, e - exp)
     else
       let c := s.get i
       if '0' ≤ c && c ≤ '9' then
-        decode (s.next i) (10*val + c.toNat - '0'.toNat) (if foundDot then e+1 else e) foundDot
-      else if c == '.' && !foundDot then
-        decode (s.next i) val e true
+        decodeAfterExp (s.next i) val e sign (10*exp + c.toNat - '0'.toNat)
       else
         none
 
-def isDecimalLit? (stx : Syntax) : Option (Nat × Nat) :=
+  decodeExp (i : String.Pos) (val : Nat) (e : Nat) : Option (Nat × Bool × Nat) :=
+    let c := s.get i
+    if c == '-' then
+       decodeAfterExp (s.next i) val e true 0
+    else
+       decodeAfterExp i val e false 0
+
+  decodeAfterDot (i : String.Pos) (val : Nat) (e : Nat) : Option (Nat × Bool × Nat) :=
+    if s.atEnd i then
+      some (val, true, e)
+    else
+      let c := s.get i
+      if '0' ≤ c && c ≤ '9' then
+        decodeAfterDot (s.next i) (10*val + c.toNat - '0'.toNat) (e+1)
+      else if c == 'e' || c == 'E' then
+        decodeExp (s.next i) val e
+      else
+        none
+
+  decode (i : String.Pos) (val : Nat) : Option (Nat × Bool × Nat) :=
+    if s.atEnd i then
+      none
+    else
+      let c := s.get i
+      if '0' ≤ c && c ≤ '9' then
+        decode (s.next i) (10*val + c.toNat - '0'.toNat)
+      else if c == '.' then
+        decodeAfterDot (s.next i) val 0
+      else if c == 'e' || c == 'E' then
+        decodeExp (s.next i) val 0
+      else
+        none
+
+def isDecimalLit? (stx : Syntax) : Option (Nat × Bool × Nat) :=
   match isLit? decimalLitKind stx with
   | some val => decodeDecimalLitVal? val
   | _        => none
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 6cbf94ccff..ec4c86ea1c 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1596,7 +1596,6 @@ def strLitKind : SyntaxNodeKind := `strLit
 def charLitKind : SyntaxNodeKind := `charLit
 def numLitKind : SyntaxNodeKind := `numLit
 def decimalLitKind : SyntaxNodeKind := `decimalLit
-def scientificLitKind : SyntaxNodeKind := `scientificLit
 def nameLitKind : SyntaxNodeKind := `nameLit
 def fieldIdxKind : SyntaxNodeKind := `fieldIdx
 def interpolatedStrLitKind : SyntaxNodeKind := `interpolatedStrLitKind
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 62315f37fe..890aa8091b 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -483,8 +483,6 @@ partial def collect : Syntax → M Syntax
       pure stx
     else if k == decimalLitKind then
       pure stx
-    else if k == scientificLitKind then
-      pure stx
     else if k == charLitKind then
       pure stx
     else if k == `Lean.Parser.Term.quotedName then
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index a7d66f4b7b..f738714a39 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1277,11 +1277,11 @@ private def mkFreshTypeMVarFor (expectedType? : Option Expr) : TermElabM Expr :=
 @[builtinTermElab decimalLit] def elabDecimalLit : TermElab := fun stx expectedType? => do
   match stx.isDecimalLit? with
   | none        => throwIllFormedSyntax
-  | some (m, e) =>
+  | some (m, sign, e) =>
     let typeMVar ← mkFreshTypeMVarFor expectedType?
     let u ← getDecLevel typeMVar
     let mvar ← mkInstMVar (mkApp (Lean.mkConst `OfDecimal [u]) typeMVar)
-    return mkApp4 (Lean.mkConst `OfDecimal.ofDecimal [u]) typeMVar mvar (mkNatLit m) (mkNatLit e)
+    return mkApp5 (Lean.mkConst `OfDecimal.ofDecimal [u]) typeMVar mvar (mkNatLit m) (toExpr sign) (mkNatLit e)
 
 @[builtinTermElab charLit] def elabCharLit : TermElab := fun stx _ => do
   match stx.isCharLit? with
diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index ed3f36ad5b..3b88a6d5ed 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -68,7 +68,7 @@ namespace Lean
 namespace Parser
 
 def isLitKind (k : SyntaxNodeKind) : Bool :=
-  k == strLitKind || k == numLitKind || k == charLitKind || k == nameLitKind || k == decimalLitKind || k == scientificLitKind
+  k == strLitKind || k == numLitKind || k == charLitKind || k == nameLitKind || k == decimalLitKind
 
 abbrev mkAtom (info : SourceInfo) (val : String) : Syntax :=
   Syntax.atom info val
@@ -807,22 +807,46 @@ partial def strLitFnAux (startPos : Nat) : ParserFn := fun c s =>
     else if curr == '\\' then andthenFn quotedCharFn (strLitFnAux startPos) c s
     else strLitFnAux startPos c s
 
-def decimalNumberFn (startPos : Nat) : ParserFn := fun c s =>
+def decimalNumberFn (startPos : Nat) (c : ParserContext) : ParserState → ParserState := fun s =>
   let s     := takeWhileFn (fun c => c.isDigit) c s
   let input := c.input
   let i     := s.pos
   let curr  := input.get i
-  if curr == '.' then
-    let i    := input.next i
-    let curr := input.get i
-    let s :=
+  if curr == '.' || curr == 'e' || curr == 'E' then
+    let s := parseOptDot s
+    let s := parseOptExp s
+    mkNodeToken decimalLitKind startPos c s
+  else
+    mkNodeToken numLitKind startPos c s
+where
+  parseOptDot s :=
+    let input := c.input
+    let i     := s.pos
+    let curr  := input.get i
+    if curr == '.' then
+      let i    := input.next i
+      let curr := input.get i
       if curr.isDigit then
         takeWhileFn (fun c => c.isDigit) c (s.setPos i)
       else
         s.setPos i
-    mkNodeToken decimalLitKind startPos c s
-  else
-    mkNodeToken numLitKind startPos c s
+    else
+      s
+
+  parseOptExp s :=
+    let input := c.input
+    let i     := s.pos
+    let curr  := input.get i
+    if curr == 'e' || curr == 'E' then
+      let i    := input.next i
+      let i    := if input.get i == '-' then input.next i else i
+      let curr := input.get i
+      if curr.isDigit then
+        takeWhileFn (fun c => c.isDigit) c (s.setPos i)
+      else
+        s.setPos i
+    else
+      s
 
 def binNumberFn (startPos : Nat) : ParserFn := fun c s =>
   let s := takeWhile1Fn (fun c => c == '0' || c == '1') "binary number" c s
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 2549cd655a..2cb0e6e232 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -27,7 +27,6 @@ builtin_initialize
   registerBuiltinNodeKind strLitKind
   registerBuiltinNodeKind numLitKind
   registerBuiltinNodeKind decimalLitKind
-  registerBuiltinNodeKind scientificLitKind
   registerBuiltinNodeKind charLitKind
   registerBuiltinNodeKind nameLitKind
 
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index bb57f94ca5..de39e99760 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -368,14 +368,26 @@ def delabOfNat : Delab := whenPPOption getPPCoercions do
   let (Expr.app (Expr.app _ (Expr.lit (Literal.natVal n) _) _) _ _) ← getExpr | failure
   return quote n
 
--- `@OfDecimal.ofDecimal _ _ m e` ~> `m*10^(-e)`
+-- `@OfDecimal.ofDecimal _ _ m s e` ~> `m*10^(sign * e)` where `sign == 1` if `s = false` and `sign = -1` if `s = true`
 @[builtinDelab app.OfDecimal.ofDecimal]
 def delabOfDecimal : Delab := whenPPOption getPPCoercions do
-  let (Expr.app (Expr.app _ (Expr.lit (Literal.natVal m) _) _) (Expr.lit (Literal.natVal e) _) _) ← getExpr | failure
+  let expr ← getExpr
+  guard <| expr.getAppNumArgs == 5
+  let Expr.lit (Literal.natVal m) _ ← pure (expr.getArg! 2) | failure
+  let Expr.lit (Literal.natVal e) _ ← pure (expr.getArg! 4) | failure
+  let s ← match expr.getArg! 3 with
+    | Expr.const `Bool.true _ _  => pure true
+    | Expr.const `Bool.false _ _ => pure false
+    | _ => failure
   let str  := toString m
-  let mStr := str.extract 0 (str.length - e)
-  let eStr := str.extract (str.length - e) str.length
-  return Syntax.mkDecimalLit (mStr ++ "." ++ eStr)
+  if s && e == str.length then
+    return Syntax.mkDecimalLit ("0." ++ str)
+  else if s && e < str.length then
+    let mStr := str.extract 0 (str.length - e)
+    let eStr := str.extract (str.length - e) str.length
+    return Syntax.mkDecimalLit (mStr ++ "." ++ eStr)
+  else
+    return Syntax.mkDecimalLit (str ++ "e" ++ (if s then "-" else "") ++ toString e)
 
 /--
 Delaborate a projection primitive. These do not usually occur in
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index 95879951d4..fd5cc71ff5 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -1464,17 +1464,25 @@ extern "C" lean_obj_res lean_float_to_string(double a) {
     return mk_string(std::to_string(a));
 }
 
-static double of_decimal(mpz const & m, size_t e) {
-    return (mpq(m)/mpz(10).pow(e)).get_double();
+static double of_decimal(mpz const & m, bool sign, size_t e) {
+    if (sign)
+        return (mpq(m)/mpz(10).pow(e)).get_double();
+    else
+        return (mpq(m)*mpz(10).pow(e)).get_double();
 }
 
-extern "C" double lean_float_of_decimal(b_lean_obj_arg m, b_lean_obj_arg e) {
-    if (!lean_is_scalar(e))
-        return 0.0;
+extern "C" double lean_float_of_decimal(b_lean_obj_arg m, uint8 esign, b_lean_obj_arg e) {
+    if (!lean_is_scalar(e)) {
+        if (esign) {
+            return 0.0;
+        } else {
+            return std::numeric_limits<double>::infinity();
+        }
+    }
     if (lean_is_scalar(m)) {
-        return of_decimal(mpz::of_size_t(lean_unbox(m)), lean_unbox(e));
+        return of_decimal(mpz::of_size_t(lean_unbox(m)), esign, lean_unbox(e));
     } else {
-        return of_decimal(mpz_value(m), lean_unbox(e));
+        return of_decimal(mpz_value(m), esign, lean_unbox(e));
     }
 }
 
diff --git a/tests/lean/decimals.lean b/tests/lean/decimals.lean
index 3625808fac..a965b6b526 100644
--- a/tests/lean/decimals.lean
+++ b/tests/lean/decimals.lean
@@ -4,3 +4,13 @@
 #eval 1.2 + 2.3
 #check 1.
 #check 3.1416
+
+theorem ex : 31416e-4 = 3.1416 :=
+  rfl
+
+#eval 3.4e-100 * 1e98
+
+#eval 12.3e90 * 1e-90
+#eval 3.00e-100 * 1e100
+#eval 3.00e-100 * 1.e100
+#eval 3.00e-100 * 1.0e100
diff --git a/tests/lean/decimals.lean.expected.out b/tests/lean/decimals.lean.expected.out
index 2cedf98c9d..4d23e3b4a3 100644
--- a/tests/lean/decimals.lean.expected.out
+++ b/tests/lean/decimals.lean.expected.out
@@ -4,3 +4,8 @@
 3.500000
 1. : Float
 3.1416 : Float
+0.034000
+12.300000
+3.000000
+3.000000
+3.000000