diff --git a/crates/ailang-prose/src/lib.rs b/crates/ailang-prose/src/lib.rs
index 3e855bb..dcfe130 100644
--- a/crates/ailang-prose/src/lib.rs
+++ b/crates/ailang-prose/src/lib.rs
@@ -908,13 +908,44 @@ fn write_pattern(out: &mut String, p: &Pattern) {
     }
 }
 
+/// Floats milestone iter 5: render a Float literal's bit pattern
+/// as surface-style decimal text. Finite values use Grisu3
+/// (`f64::to_string`) with a `.0` suffix when neither `.` nor
+/// `e`/`E` appears, parallel to
+/// `crates/ailang-surface/src/print.rs::write_float_lit`. Non-finite
+/// values render as `NaN` / `+Inf` / `-Inf` — these are valid in
+/// Form-A (the canonical bytes carry the bit pattern) but cannot
+/// be expressed in surface lex; prose is one-way render, so naming
+/// them after the Mainstream-language spellings is more useful
+/// than a panic or a `(float-bits hex)` placeholder.
+fn write_float_lit(out: &mut String, bits: u64) {
+    let f = f64::from_bits(bits);
+    if f.is_nan() {
+        out.push_str("NaN");
+        return;
+    }
+    if f == f64::INFINITY {
+        out.push_str("+Inf");
+        return;
+    }
+    if f == f64::NEG_INFINITY {
+        out.push_str("-Inf");
+        return;
+    }
+    let s = f.to_string();
+    out.push_str(&s);
+    if !s.contains('.') && !s.contains('e') && !s.contains('E') {
+        out.push_str(".0");
+    }
+}
+
 fn write_lit(out: &mut String, lit: &Literal) {
     match lit {
         Literal::Int { value } => out.push_str(&value.to_string()),
         Literal::Bool { value } => out.push_str(if *value { "true" } else { "false" }),
         Literal::Str { value } => write_string_lit(out, value),
         Literal::Unit => out.push_str("()"),
-        Literal::Float { .. } => unimplemented!("Floats milestone iter 5: prose"),
+        Literal::Float { bits } => write_float_lit(out, *bits),
     }
 }
 
@@ -1189,6 +1220,46 @@ mod tests {
         assert_eq!(render_term(&Term::Lit { lit: Literal::Unit }), "()");
     }
 
+    /// Floats milestone iter 5.1: prose renders Float literals as
+    /// surface-style decimal text. Finite values use shortest
+    /// round-trippable decimal with `.0` suffix when neither `.` nor
+    /// `e`/`E` is in the rendered string (parallel to surface print).
+    /// Non-finite (NaN, ±Inf) render as the Mainstream-language
+    /// spellings — `NaN`, `+Inf`, `-Inf` — because prose is a one-way
+    /// render and the surface lex grammar's no-NaN/Inf restriction
+    /// does not apply to it.
+    #[test]
+    fn renders_float_literal_finite() {
+        use ailang_core::ast::*;
+        let t = Term::Lit { lit: Literal::Float { bits: 0x3ff8_0000_0000_0000u64 } };
+        let s = render_term(&t);
+        assert_eq!(s, "1.5");
+
+        let t = Term::Lit { lit: Literal::Float { bits: 0x4024_0000_0000_0000u64 } };
+        let s = render_term(&t);
+        assert_eq!(s, "10.0");
+    }
+
+    #[test]
+    fn renders_float_literal_signed_zero() {
+        use ailang_core::ast::*;
+        let pos = Term::Lit { lit: Literal::Float { bits: 0x0u64 } };
+        assert_eq!(render_term(&pos), "0.0");
+        let neg = Term::Lit { lit: Literal::Float { bits: 0x8000_0000_0000_0000u64 } };
+        assert_eq!(render_term(&neg), "-0.0");
+    }
+
+    #[test]
+    fn renders_float_literal_non_finite() {
+        use ailang_core::ast::*;
+        let nan = Term::Lit { lit: Literal::Float { bits: 0x7ff8_0000_0000_0000u64 } };
+        assert_eq!(render_term(&nan), "NaN");
+        let pos_inf = Term::Lit { lit: Literal::Float { bits: 0x7ff0_0000_0000_0000u64 } };
+        assert_eq!(render_term(&pos_inf), "+Inf");
+        let neg_inf = Term::Lit { lit: Literal::Float { bits: 0xfff0_0000_0000_0000u64 } };
+        assert_eq!(render_term(&neg_inf), "-Inf");
+    }
+
     #[test]
     fn var_renders_as_name() {
         assert_eq!(render_term(&Term::Var { name: "x".into() }), "x");